This project is read-only.

Abstract Methods

Jun 29, 2010 at 12:01 AM

Hi,

 I am trying to specify an abstract method and marking it as Pure to use it in specifying other classes. I get a verifier error stating that method purity cannot be verified.

An example would be the definition of a stack top method:

 public /*@ pure @*/ abstract Object top( );

in http://www.eecs.ucf.edu/~leavens/JML/prelimdesign/prelimdesign_2.html#SEC12

How can this be done in Spec#?

Thanks,

 

Iman

Jun 29, 2010 at 2:18 AM

Hello Iman,

What you're trying to do is alarmingly difficult in Spec#.

One major thing that makes this difficult is that Spec# does not build in theory types, nor does not provide a practical way to provide user-defined theory types.

A second major thing that makes this difficult, and this is more specifically what you're seeing in the error message, is that Spec# wants to make sure the pure methods in your program do not give rise to inconsistent axioms in the verifier.  Doing so involves producing a witness that shows the ensures clause to be attainable.  The place where we usually see this break is when the return type is of a non-null type.  In your case, you can change the return types to object?, but you will still see trouble because you have to decide if theStack, which is an object, should be [Rep] or [Peer].  [Peer] may seem the natural choice, because you're not hiding theStack as an implementation detail, but using [Peer] won't let you write the specifications that dereference theStack.  On the other hand, [Rep] will cause the problem when proving the consistency of Top(), because that proof needs the axiom about the pure method First, and Spec# conservatively turns off all pure-method axioms while checking the consistency of other pure methods.

Things get a little better if you use a struct instead of a class for the "theory value".  Still, no cigar.

Since I wrote them anyway, I'm including below my attempts at doing this with a class and a struct, respectively.  However, neither program verifies.  (The struct version happened upon a bug in SscBoogie, for which I just checked in a fix.)

(Shameless plug:  The language and verifier Dafny has significantly better support for these things, though it does not include subclassing.)

----------  class version  ----------

using Microsoft.Contracts;

[Verify(false)]
public abstract class JMLObjectSequence {
  [Pure]
  public abstract bool IsEmpty();
  [Pure]
  public abstract JMLObjectSequence Trailer();
  [Pure]
  public abstract JMLObjectSequence InsertFront(object? x);
  [Pure] [ResultNotNewlyAllocated]
  public abstract object? First();
}
[Verify(false)]
public sealed class Default_JMLObjectSequence : JMLObjectSequence {
  [NotDelayed]
  public Default_JMLObjectSequence()
    ensures IsEmpty();
  {
  }
  [Pure]
  public override bool IsEmpty() { return true; } // bogus
  [Pure]
  public override JMLObjectSequence Trailer() { return this; }  // bogus
  [Pure]
  public override JMLObjectSequence InsertFront(object? x) { return this; }  // bogus
  [Pure] [ResultNotNewlyAllocated]
  public override object? First() { return this; }  // bogus
}

public abstract class UnboundedStack {

  [SpecPublic] [Rep]
  public JMLObjectSequence theStack;

  [NotDelayed]
  public UnboundedStack()
    ensures theStack.IsEmpty();
  {
    theStack = new Default_JMLObjectSequence();
    base();
  }

  public abstract void Pop();
    requires !theStack.IsEmpty();
    modifies theStack;
    ensures theStack.Equals(old(theStack.Trailer()));

  public abstract void Push(object? x);
    modifies theStack;
    ensures theStack.Equals(old(theStack.InsertFront(x)));

  [Pure]
  public abstract object? Top();
    requires !theStack.IsEmpty();
    ensures result == theStack.First();
}

----------  struct version  ----------

using Microsoft.Contracts;

public struct JMLObjectSequence {
  [Pure] public bool IsEmpty()
    ensures true;
  { return false; }

  [Pure]
  public JMLObjectSequence Trailer()
    ensures true;
  { return this; }  // bogus

  [Pure]
  public JMLObjectSequence InsertFront(object? x)
    ensures true;
  { return this; }  // bogus

  [Pure] [ResultNotNewlyAllocated]
  public object? First()
    ensures true;
  { return null; }  // bogus

  [Pure]
  public override bool Equals(object? other)
    ensures true;
  { return false; }  // bogus
}

public abstract class UnboundedStack {

  [SpecPublic]
  public JMLObjectSequence theStack;

  [NotDelayed]
  public UnboundedStack()
    ensures theStack.IsEmpty();
  {
    assume theStack.IsEmpty();
  }

  public abstract void Pop();
    requires !theStack.IsEmpty();
    modifies theStack;
    ensures theStack.Equals(old(theStack.Trailer()));

  public abstract void Push(object? x);
    modifies theStack;
    ensures theStack.Equals(old(theStack.InsertFront(x)));

  [Pure]
  public abstract object? Top();
    requires !theStack.IsEmpty();
    ensures result == theStack.First();
}

Aug 23, 2010 at 6:05 AM

Thanks for the comprehensive reply. I am currently experimenting with Dafny.

I am wondering is there an editor for the Dafny language?

Thanks,

Iman

Aug 24, 2010 at 4:07 AM

I found the editor I was looking for, for anyone interested refer to: http://boogie.codeplex.com/wikipage?title=Sources&referringTitle=Home

 

 

Aug 24, 2010 at 4:27 AM

 

Is there a reason why functions in Dafny cannot have an ensures clause in their specs?

 

Thanks,

 

Iman

Mar 4, 2011 at 6:21 PM

For what it's worth..

My understanding (which is based on Chalice, but I suspect it's the same in Dafny) is that function bodies are effectively their own post-conditions (i.e., you know exactly what the function does, by seeing its body). Of course, this doesn't give you information hiding with respect to the implementation details, but I don't think Dafny has a notion of visibility for function definitions anyway.

Cheers,

Alex