diff options
Diffstat (limited to 'Test/hofs/Frame.dfy')
-rw-r--r-- | Test/hofs/Frame.dfy | 128 |
1 files changed, 128 insertions, 0 deletions
diff --git a/Test/hofs/Frame.dfy b/Test/hofs/Frame.dfy new file mode 100644 index 00000000..891435ba --- /dev/null +++ b/Test/hofs/Frame.dfy @@ -0,0 +1,128 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + + +class C { var u : int; } + +method M(f : int -> int) + requires f.requires(0); +{ + var init := f(0); + var o := new C; + assert init == f(0); +} + +method M2() +{ + var c := new C; + c.u := 0; + var f := () reads c => c.u; + var init := f(); + c.u := 1; + if * { + assert f() == init; // should fail + } else { + assert f() == 1; + } +} + +method M3() +{ + var c := new C; + c.u := 0; + var f := () reads c => c.u; + assert f() == 0; + c.u := 1; + assert f() == 1; + assert f() == 0; // should fail + assert false; // should fail +} + +method Main() { + var x := 2; + var getX := () => x; + assert getX() == 2; + x := 3; + assert getX() == 2; // the value is copied +} + +method Refs() { + var a := new int[1]; + a[0] := 2; + var get; + if * { + + get := () reads a => a[0]; // OK + assert get() == 2; + + a[0] := 3; + assert get() == 3; // OK, the ref is copied, but not the entire array + + a := new int[0]; + assert get() == 3; // OK, still 3 + assert get() == 0 || get() == 2; // fail: is three! + + } else if * { + get := () => a[0]; // fail: Not enough read + } else { + get := () reads {} => a[0]; // fail: Not enough read + } +} + +method Fiddling(k : int -> int) +{ + + var mkGet := (arr : array<int>) => + () reads arr requires arr != null requires arr.Length > 0 => arr[0]; + + var a := new int[1]; + var b := new int[1]; + + var get := mkGet(a); + + a[0] := 0; + b[0] := 10; + + assert get() == a[0]; + + b[0] := 20; + + assert get() == a[0]; +} + +method HeapSucc0(k : int -> int) + requires k.requires(0); +{ + var init := k(0); + var a := new object; + assert k(0) == init; +} + +method HeapSucc1(k : int -> int, c : C) + requires k.requires(0); + requires c !in k.reads(0); + modifies c; +{ + var init := k(0); + if ( c != null ) { + c.u := c.u + 1; + assert k(0) == init; + } +} + +method HeapSucc2(k : int -> int, c : C) + requires k.requires(0); + modifies c; +{ + var init := k(0); + if ( c != null ) { + c.u := c.u + 1; + if ( c !in k.reads(0) ) { + assert k(0) == init; + } else { + assert k(0) == init; // Fail + } + } +} + + |