Object invariant - a simple subset relationship

Sep 29, 2012 at 5:46 PM

Thanks for your help in an earlier thread. I do now have Spec# installed in my office without problems (though not in the labs yet) and I have tried writing my first example. I would like to define as an invariant a simple subset  relationship between two arrays (see below) but I am told the relationship may not hold an after initialising to particular constants where the relationship is clearly true.

This is by umpteenth attempt to write this. All the others have produced error messages for one reason or the other, so I would appreciate it if you could tell me whether I should have been able to do what I was trying to do.

1. I would like to use sets for this except that I understand the sets were introduced into C# too late (I have Visual Studio 2010).

2. I wanted to avoid indices too by using this:

 invariant forall{int ii in a; exists{jj in b; ii.Equals(jj)}};

but I then learned I needed to use Custom Attribute Contacts.Pure - does this mean editting the library code that defines equality on Strings?

3. I tried using List too but I got a "must be owned by self" error even though I used [Rep] to indicate an aggregation.

-------------------------------------------------------------------------------------------------------------------------------------------

using System;
using Microsoft.Contracts;

public class Program
{


  class State {

     invariant forall{int i in (0: a.Length); exists{int j in (0: b.Length);a[i].Equals(b[j])}};
     invariant a[0].Equals(b[0]); // array index possibly above bound??
     invariant forall{int i in (0: a.Length); a[i].Equals("hello")}; // True


     [Rep] string[] a = {"hello"};
     [Rep] string[] b = {"hello", "world", "bye"};

     public State() {

     }

  }

  static void Main(string![]! args) {
     Console.WriteLine("hello".Equals("hello")); // True
     Console.ReadLine();

  }
}

Sep 29, 2012 at 6:16 PM

This problem somehow disappeared when I created a new project and copy-and-pasted. Then I got errors about nullness which I fixed:

[Rep] string![]! a = {"hello"};

However, can you tell me please if I should be able to use List or Set and if I should be able to use the other form of the invariant quoted above?

Coordinator
Oct 16, 2012 at 1:42 AM

It's tricky to use .Equals in specifications, because of what it may read.  Hopefully, the error messages will guide you to ways of representing what you want.

If your program has a List or Set class, Spec# would be able to use them.  As you have run into, Spec# is a superset of C# 2.0, so many of the syntax enhancements in newer versions of C# are not available in Spec#.

By the way, I'm guessing you're using Spec# for the run-time checking?  I'd be interested in learing more about what your aim is.  For example, if you want to teach writing contracts and getting run-time checking, then it's possible that Code Contracts in .NET (which you can use with the latest C#) would suit your needs.  If, on the other hand, you're trying to do more serious static verification, then have you considered using Dafny (http://research.microsoft.com/dafny)?

  Rustan

Oct 16, 2012 at 4:24 PM
Hi Rustan,

Thanks for your thoughts. I was thinking about having a class that
represents the state of a scrabble game. Thinking about it in Z
terminology, there is a set of tiles in a bag (or even a bag of tiles
in a bag), two size-7 sets on two racks and a partial function from
{0..WIDTH-1} x {0..WIDTH-1} to tile, commonly called a 2D array. Tiles
could be characters but perhaps should be tagged to keep tiles unique
eg the 1st A, 2nd A etc. An important decision but one yet to be made.
I'm keeping it open because maybe Spec# would be better with
primitives, though counting the A's would be a bit tricky.

I don't know whether this is an appropriate use of Spec# but you could
have an object invariant that says every tile must have been in the
bag originally and every tile that was in the bag has not "fallen
under the table" ie it's still in the bag, on a rack or on the board.
Except for the board, I certainly want sets (but I think they were
introduced to C# later than 2.0 and I can't use later libraries).
However, even if I can't have sets, I want to model sets as 1D arrays
and be able to test for subset inclusion. I thought I would write a
method to check for this, so I could then use it in the object
invariant. That's why you see the method I've shown you.

I'm not really experienced enough with Spec# to know what I can expect
it to do for me but maybe you can tell me how this sounds. Also, on a
minor, more easily correctable point, I don't know if I should be
using == or Equals, but I had no luck with == either; I'm sure I have
bigger problems that just that though.

Ian
Coordinator
Oct 17, 2012 at 10:59 PM

Sounds like a nice exercise.  Are you hoping to (statically) verify properties about the program, or is your focus the writing of the specifications (and perhaps getting run-time checks)?

If it's the latter, then Spec# is probably fine.  The ownership of the tiles will require some care.  I don't remember, but I think Spec# does this better (or only?) for single-dimensional arrays.  If it is possible for you to represent the tiles as integers, you'll avoid both the == vs. .Equals issue as well as ownership issues.

If it's the former (that is, you want to verify the program statically), then Dafny will be a much better choice.  You can also compile and execute Dafny programs, but there are no UI libraries, for example.  (I'd be delighted if someone would write such libraries for Dafny, even simple ones.)

  Rustan