Frame question for non-inlined method calls

Oct 21, 2010 at 10:26 PM

Hi,

I'm new to Spec# and I'm confused about a case involving an array field

and a call to method which is not inlined.

In m1 method below this.fa is an array and precondition is this.fa[0] == 42.

m1 takes one int[] a as argument. it calls another method aSet which sets a[0] to 5.

the method is not inlined so its post condition/modifies clause would be used for

vc purposes. aSet has a frame condition of "modifies a[0]".

Why is it that after this method call, the assertion this.fa[0] == 42 fails?

In other words, how should I express the fact that fields of "this" after a call to the

static method aSet() are not changed, without explicitly making that a post condition of

aSet()? Even if I make aSet() non-static and include "modifies this.0" the same happens.

The instance is below.

Thanks!

Hesam

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

FrameTest.ssc(15,2): Error: Assertion might not hold: this.fa[0] == 42

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

using Microsoft.Contracts;

class FrameTest {

    int[] fa;

    void m1(int[]! a)
     modifies a[0], this.0;
         requires this.fa != a;
         requires a.Length > 0;
         requires this.fa.Length > 0;
         requires this.fa[0] == 42;
    {
    aSet(a);
    assert this.fa[0] == 42;
    }

    static void aSet(int[]! a)
        requires a.Length > 0;
        modifies a[0];
        ensures a[0] == 5;
    {
    a[0] = 5;
    }

    [Verify(false)]
    public static void Main(string[] args) { }

}

Developer
Oct 26, 2010 at 2:54 PM

Hi Hesam,

Spec# allows a method to modify objects whose owner is not exposed. In your example, Spec# does not know who owns the array object fa. In particular, its owner could be not exposed when aSet is called and, thus, the method might change the contents of fa. You can fix this problem for instance by declaring fa with the attribute [Peer], which expresses that the array object has the same owner as "this", which by default is required to have an exposed owner. Alternatively, you could add a precondition " fa.IsConsistent" to m1, which also expresses that fa's owner is exposed. Both options work for me.

Cheers,
   Peter

Oct 29, 2010 at 7:30 PM

Thanks very much Peter. Makes sense, and both work for me as well. Cheers, -Hesam