From 4cbe4583b329a39dee2b4b456758cafbe7e2fa79 Mon Sep 17 00:00:00 2001 From: Dan Rosén Date: Mon, 11 Aug 2014 14:57:27 -0700 Subject: Add higher-order-functions and some other goodies * The reads clause now needs to be self framing. * The requires clause now needs to be framed by the reads clause. * There are one-shot lambdas, with a single arrow, but they will probably be removed. * There is a {:heapQuantifier} attribute to quantifiers, but they will probably be removed. * Add smart handling of type variables * Add < and > for datatype & type parameter --- Test/hofs/Apply.dfy | 29 +++++ Test/hofs/Apply.dfy.expect | 7 ++ Test/hofs/Classes.dfy | 50 ++++++++ Test/hofs/Classes.dfy.expect | 10 ++ Test/hofs/Consequence.dfy | 9 ++ Test/hofs/Consequence.dfy.expect | 2 + Test/hofs/Examples.dfy | 59 ++++++++++ Test/hofs/Examples.dfy.expect | 2 + Test/hofs/Field.dfy | 23 ++++ Test/hofs/Field.dfy.expect | 14 +++ Test/hofs/FnRef.dfy | 70 +++++++++++ Test/hofs/FnRef.dfy.expect | 27 +++++ Test/hofs/Frame.dfy | 128 ++++++++++++++++++++ Test/hofs/Frame.dfy.expect | 38 ++++++ Test/hofs/Lambda.dfy | 60 ++++++++++ Test/hofs/Lambda.dfy.expect | 14 +++ Test/hofs/LambdaParsefail.dfy | 33 ++++++ Test/hofs/LambdaParsefail.dfy.expect | 5 + Test/hofs/LambdaParsefail2.dfy | 8 ++ Test/hofs/LambdaParsefail2.dfy.expect | 2 + Test/hofs/Map.dfy | 117 ++++++++++++++++++ Test/hofs/MutableField.dfy | 15 +++ Test/hofs/MutableField.dfy.expect | 2 + Test/hofs/Naked.dfy | 51 ++++++++ Test/hofs/Naked.dfy.expect | 50 ++++++++ Test/hofs/OneShot.dfy | 25 ++++ Test/hofs/OneShot.dfy.expect | 20 ++++ Test/hofs/Quant.dfy | 132 +++++++++++++++++++++ Test/hofs/ReadsReads.dfy | 59 ++++++++++ Test/hofs/ReadsReads.dfy.expect | 18 +++ Test/hofs/Renaming.dfy | 25 ++++ Test/hofs/Renaming.dfy.expect | 2 + Test/hofs/ResolveError.dfy | 51 ++++++++ Test/hofs/ResolveError.dfy.expect | 14 +++ Test/hofs/Simple.dfy | 90 ++++++++++++++ Test/hofs/Simple.dfy.expect | 32 +++++ Test/hofs/TreeMap.dfy | 215 ++++++++++++++++++++++++++++++++++ Test/hofs/TreeMapSimple.dfy | 49 ++++++++ Test/hofs/TreeMapSimple.dfy.expect | 2 + Test/hofs/Twice.dfy | 38 ++++++ Test/hofs/Twice.dfy.expect | 11 ++ Test/hofs/Types.dfy | 20 ++++ Test/hofs/Types.dfy.expect | 4 + Test/hofs/WhileLoop.dfy | 50 ++++++++ Test/hofs/WhileLoop.dfy.expect | 2 + 45 files changed, 1684 insertions(+) create mode 100644 Test/hofs/Apply.dfy create mode 100644 Test/hofs/Apply.dfy.expect create mode 100644 Test/hofs/Classes.dfy create mode 100644 Test/hofs/Classes.dfy.expect create mode 100644 Test/hofs/Consequence.dfy create mode 100644 Test/hofs/Consequence.dfy.expect create mode 100644 Test/hofs/Examples.dfy create mode 100644 Test/hofs/Examples.dfy.expect create mode 100644 Test/hofs/Field.dfy create mode 100644 Test/hofs/Field.dfy.expect create mode 100644 Test/hofs/FnRef.dfy create mode 100644 Test/hofs/FnRef.dfy.expect create mode 100644 Test/hofs/Frame.dfy create mode 100644 Test/hofs/Frame.dfy.expect create mode 100644 Test/hofs/Lambda.dfy create mode 100644 Test/hofs/Lambda.dfy.expect create mode 100644 Test/hofs/LambdaParsefail.dfy create mode 100644 Test/hofs/LambdaParsefail.dfy.expect create mode 100644 Test/hofs/LambdaParsefail2.dfy create mode 100644 Test/hofs/LambdaParsefail2.dfy.expect create mode 100644 Test/hofs/Map.dfy create mode 100644 Test/hofs/MutableField.dfy create mode 100644 Test/hofs/MutableField.dfy.expect create mode 100644 Test/hofs/Naked.dfy create mode 100644 Test/hofs/Naked.dfy.expect create mode 100644 Test/hofs/OneShot.dfy create mode 100644 Test/hofs/OneShot.dfy.expect create mode 100644 Test/hofs/Quant.dfy create mode 100644 Test/hofs/ReadsReads.dfy create mode 100644 Test/hofs/ReadsReads.dfy.expect create mode 100644 Test/hofs/Renaming.dfy create mode 100644 Test/hofs/Renaming.dfy.expect create mode 100644 Test/hofs/ResolveError.dfy create mode 100644 Test/hofs/ResolveError.dfy.expect create mode 100644 Test/hofs/Simple.dfy create mode 100644 Test/hofs/Simple.dfy.expect create mode 100644 Test/hofs/TreeMap.dfy create mode 100644 Test/hofs/TreeMapSimple.dfy create mode 100644 Test/hofs/TreeMapSimple.dfy.expect create mode 100644 Test/hofs/Twice.dfy create mode 100644 Test/hofs/Twice.dfy.expect create mode 100644 Test/hofs/Types.dfy create mode 100644 Test/hofs/Types.dfy.expect create mode 100644 Test/hofs/WhileLoop.dfy create mode 100644 Test/hofs/WhileLoop.dfy.expect (limited to 'Test/hofs') diff --git a/Test/hofs/Apply.dfy b/Test/hofs/Apply.dfy new file mode 100644 index 00000000..bdd102c2 --- /dev/null +++ b/Test/hofs/Apply.dfy @@ -0,0 +1,29 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + + +method Apply(x : int) returns (i : int) + ensures i == x; +{ + i := (x => x)(x); +} + +function method Const(a : A) : B -> A { + b => a +} + +method Test(m : map int -> int>) +{ + assume forall i :: i in m; + assume forall i, x :: m[i].requires(x); + assume forall i, x, y :: m[i](x).requires(y); + assume m[1](2)(3) > 5; + assert ((m[1])(2))(3) > 4; +} + +method Main() { + assert forall x : int, y : int :: Const(x)(y) == (Const(x))(y); + assert (a => b => a) == (u : int) => (v : int) => u; + assert Const == (u : int) => (v : int) => u; +} + diff --git a/Test/hofs/Apply.dfy.expect b/Test/hofs/Apply.dfy.expect new file mode 100644 index 00000000..fad1fe33 --- /dev/null +++ b/Test/hofs/Apply.dfy.expect @@ -0,0 +1,7 @@ +Apply.dfy(27,16): Error: assertion violation +Execution trace: + (0,0): anon0 + Apply.dfy(26,35): anon15_Else + Apply.dfy(27,27): anon17_Else + +Dafny program verifier finished with 6 verified, 1 error diff --git a/Test/hofs/Classes.dfy b/Test/hofs/Classes.dfy new file mode 100644 index 00000000..91d7e384 --- /dev/null +++ b/Test/hofs/Classes.dfy @@ -0,0 +1,50 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + + +class C { + static function method Static() : bool + { + true + } +} + +method K() { + var f := C.Static; + var o : object; + assert o !in f.reads(); + assert f.requires(); + assert f(); +} + + +class T { + var h : int -> int; +} + +function B(t : T) : int -> int + requires t != null; + reads t; +{ + t.h +} + +function J(t : T) : int + requires t != null; + requires t.h.reads(0) == {}; + reads t; + reads if t != null then t.h.reads(0) else {}; +{ + if t.h.requires(0) then + B(t)(0) + else + B(t)(0) // fail +} + +method U(t : T) + requires t != null; + modifies t; +{ + t.h := x => x; + assert J(t) == 0; // ok +} diff --git a/Test/hofs/Classes.dfy.expect b/Test/hofs/Classes.dfy.expect new file mode 100644 index 00000000..84a0417e --- /dev/null +++ b/Test/hofs/Classes.dfy.expect @@ -0,0 +1,10 @@ +Classes.dfy(41,5): Error: possible violation of function precondition +Execution trace: + (0,0): anon0 + (0,0): anon11_Then + (0,0): anon3 + (0,0): anon12_Then + (0,0): anon13_Else + (0,0): anon14_Else + +Dafny program verifier finished with 6 verified, 1 error diff --git a/Test/hofs/Consequence.dfy b/Test/hofs/Consequence.dfy new file mode 100644 index 00000000..35934470 --- /dev/null +++ b/Test/hofs/Consequence.dfy @@ -0,0 +1,9 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +method Check() { + var f : nat -> nat; + assume f.requires(0); + var i : nat := f(0); +} + diff --git a/Test/hofs/Consequence.dfy.expect b/Test/hofs/Consequence.dfy.expect new file mode 100644 index 00000000..069e7767 --- /dev/null +++ b/Test/hofs/Consequence.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 2 verified, 0 errors diff --git a/Test/hofs/Examples.dfy b/Test/hofs/Examples.dfy new file mode 100644 index 00000000..c31b68da --- /dev/null +++ b/Test/hofs/Examples.dfy @@ -0,0 +1,59 @@ +// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function Apply(f: A -> B, x: A): B + reads f.reads(x); + requires f.requires(x); +{ + f(x) +} + +function Apply'(f: A -> B) : A -> B +{ + x reads f.reads(x) + requires f.requires(x) + => f(x) +} + + +function Compose(f: B -> C, g:A -> B): A -> C +{ + x reads g.reads(x) + reads if g.requires(x) then f.reads(g(x)) else {} + requires g.requires(x) + requires f.requires(g(x)) + => f(g(x)) +} + +function W(f : (A,A) -> A): A -> A +{ + x requires f.requires(x,x) + reads f.reads(x,x) + => f(x,x) +} + +function Curry(f : (A,B) -> C) : A -> B -> C +{ + x => y requires f.requires(x,y) + reads f.reads(x,y) + => f(x,y) +} + +function Uncurry(f : A -> B -> C) : (A,B) -> C +{ + (x,y) requires f.requires(x) + requires f(x).requires(y) + reads f.reads(x) + reads if f.requires(x) then f(x).reads(y) else {} + => f(x)(y) +} + +function S(f : (A,B) -> C, g : A -> B): A -> C +{ + x requires g.requires(x) + requires f.requires(x,g(x)) + reads g.reads(x) + reads if g.requires(x) then f.reads(x,g(x)) else {} + => f(x,g(x)) +} + diff --git a/Test/hofs/Examples.dfy.expect b/Test/hofs/Examples.dfy.expect new file mode 100644 index 00000000..76f19e0d --- /dev/null +++ b/Test/hofs/Examples.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 7 verified, 0 errors diff --git a/Test/hofs/Field.dfy b/Test/hofs/Field.dfy new file mode 100644 index 00000000..6d3412d7 --- /dev/null +++ b/Test/hofs/Field.dfy @@ -0,0 +1,23 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// calling fields should not make a resolution error: + +class Ref { + var val: A; +} + +method Nope() { + var f := new Ref bool>; + assert f.val(0); +} + +class FnRef { + var fn: A -> B; +} + +method Nope2() { + var f := new FnRef; + assert f.fn(0); +} + diff --git a/Test/hofs/Field.dfy.expect b/Test/hofs/Field.dfy.expect new file mode 100644 index 00000000..927d8b06 --- /dev/null +++ b/Test/hofs/Field.dfy.expect @@ -0,0 +1,14 @@ +Field.dfy(12,10): Error: assertion violation +Execution trace: + (0,0): anon0 +Field.dfy(12,12): Error: possible violation of function precondition +Execution trace: + (0,0): anon0 +Field.dfy(21,10): Error: assertion violation +Execution trace: + (0,0): anon0 +Field.dfy(21,12): Error: possible violation of function precondition +Execution trace: + (0,0): anon0 + +Dafny program verifier finished with 2 verified, 4 errors diff --git a/Test/hofs/FnRef.dfy b/Test/hofs/FnRef.dfy new file mode 100644 index 00000000..fb8136b7 --- /dev/null +++ b/Test/hofs/FnRef.dfy @@ -0,0 +1,70 @@ +// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + + +class Ref { + var val: A; +} + +method Nope() { + var f : Ref bool>; + var g : int -> bool; + + f := new Ref bool>; + + f.val := x => true; + + g := x reads f reads f.val.reads(x) => !f.val(x); +} + +method M() { + var f : Ref bool>; + var g : int -> bool; + + f := new Ref bool>; + + f.val := x => true; + + g := x reads f reads f.val.reads(x) requires f.val.requires(x) => !f.val(x); + + f.val := g; + + if (!g(0)) { + assert !g(0); + } else { + assert g(0); + } +} + + +method L() { + var f : Ref<() -> bool>; + f := new Ref<() -> bool>; + f.val := () reads f reads f.val.reads() requires !f.val.requires() => true; + + if (f.val.requires()) { + assert !f.val.requires(); + } else { + assert f.val.requires(); + } +} + +method LRead() { + var o : object; + var f : Ref<() -> bool>; + f := new Ref<() -> bool>; + f.val := () reads f + reads f.val.reads() + reads if o in f.val.reads() then {} else {o} + => true; + + assume o != null; + assert o != f; + + if (o in f.val.reads()) { + assert o !in f.val.reads(); + } else { + assert o in f.val.reads(); + } +} + diff --git a/Test/hofs/FnRef.dfy.expect b/Test/hofs/FnRef.dfy.expect new file mode 100644 index 00000000..5185c21c --- /dev/null +++ b/Test/hofs/FnRef.dfy.expect @@ -0,0 +1,27 @@ +FnRef.dfy(17,45): Error: possible violation of function precondition +Execution trace: + (0,0): anon0 + FnRef.dfy(15,12): anon5_Else + (0,0): anon6_Then +FnRef.dfy(32,8): Error: possible violation of function precondition +Execution trace: + (0,0): anon0 + FnRef.dfy(26,12): anon9_Else + FnRef.dfy(28,8): anon10_Else +FnRef.dfy(46,12): Error: assertion violation +Execution trace: + (0,0): anon0 + FnRef.dfy(43,13): anon7_Else + (0,0): anon9_Then +FnRef.dfy(65,14): Error: assertion violation +Execution trace: + (0,0): anon0 + FnRef.dfy(56,13): anon8_Else + (0,0): anon10_Then +FnRef.dfy(67,14): Error: assertion violation +Execution trace: + (0,0): anon0 + FnRef.dfy(56,13): anon8_Else + (0,0): anon10_Else + +Dafny program verifier finished with 4 verified, 5 errors 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) => + () 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 + } + } +} + + diff --git a/Test/hofs/Frame.dfy.expect b/Test/hofs/Frame.dfy.expect new file mode 100644 index 00000000..a4d10c47 --- /dev/null +++ b/Test/hofs/Frame.dfy.expect @@ -0,0 +1,38 @@ +Frame.dfy(23,16): Error: assertion violation +Execution trace: + (0,0): anon0 + Frame.dfy(19,13): anon5_Else + (0,0): anon6_Then +Frame.dfy(37,14): Error: assertion violation +Execution trace: + (0,0): anon0 + Frame.dfy(33,13): anon3_Else +Frame.dfy(63,23): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon13_Then + Frame.dfy(55,13): anon14_Else + (0,0): anon15_Then + (0,0): anon5 +Frame.dfy(66,19): Error: insufficient reads clause to read array element +Execution trace: + (0,0): anon0 + (0,0): anon16_Then + (0,0): anon17_Then +Frame.dfy(68,28): Error: insufficient reads clause to read array element +Execution trace: + (0,0): anon0 + (0,0): anon16_Else + (0,0): anon18_Then +Frame.dfy(123,14): Error: possible violation of function precondition +Execution trace: + (0,0): anon0 + (0,0): anon5_Then + (0,0): anon6_Else +Frame.dfy(123,19): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon5_Then + (0,0): anon6_Else + +Dafny program verifier finished with 14 verified, 7 errors diff --git a/Test/hofs/Lambda.dfy b/Test/hofs/Lambda.dfy new file mode 100644 index 00000000..44adb4ce --- /dev/null +++ b/Test/hofs/Lambda.dfy @@ -0,0 +1,60 @@ +// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + + +method M() { + var f1 : A -> A := x => x; + var f2 : A -> A := (x) => x; + var f3 : () -> () := () => (); + var tt : () := (); + var f4 : (A, A) -> (A, A) := (x, y) => (y, x); + var f5 := (x : int) => x; + + var f6 := x requires x != 0 requires x != 1 => x; + var f7 := x requires 0 != x requires x != 1 => x; + assert f6(2) == f7(2); + + var u := 0; + var f8 := () requires u == 0 => true; + assert f8(); + u := 1; + assert f8(); // ok, u value is copied at creation of f8 + + var f9 := () requires u == 0 => true; + assert !f9.requires(); + +} + +datatype List = Cons(A,List) | Nil + +method J(xs : List) returns (z : int) { + match xs + case Cons(y,ys) => z := y; + case Nil => z := 0; + + if { + case true => z := z; + case true => z := 1; + } +} + +function Adder() : (int, int) -> int + ensures forall x, y :: Adder().requires(x, y); + ensures forall x, y :: (Adder())(x, y) == x + y; +{ + (x, y) => x + y +} + +function MkId() : A -> A +{ + x => x +} + + +// storage and references to functions +method T() { + var f := x => x + 1; + f := u => if u > 0 then f(u) else u; + assert f(1) == 2 && f(0) == 0; +} + diff --git a/Test/hofs/Lambda.dfy.expect b/Test/hofs/Lambda.dfy.expect new file mode 100644 index 00000000..a32c27ff --- /dev/null +++ b/Test/hofs/Lambda.dfy.expect @@ -0,0 +1,14 @@ +Lambda.dfy(24,12): Error: assertion violation +Execution trace: + (0,0): anon0 + Lambda.dfy(6,24): anon31_Else + Lambda.dfy(7,26): anon32_Else + Lambda.dfy(8,27): anon33_Else + Lambda.dfy(10,39): anon34_Else + Lambda.dfy(11,23): anon35_Else + Lambda.dfy(13,15): anon36_Else + Lambda.dfy(14,15): anon39_Else + Lambda.dfy(18,16): anon42_Else + Lambda.dfy(23,16): anon44_Else + +Dafny program verifier finished with 7 verified, 1 error diff --git a/Test/hofs/LambdaParsefail.dfy b/Test/hofs/LambdaParsefail.dfy new file mode 100644 index 00000000..1d864d73 --- /dev/null +++ b/Test/hofs/LambdaParsefail.dfy @@ -0,0 +1,33 @@ +// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +method Fails() { + var g1 := x.x => x; // fail + var g2 := x() => x; // fail + var g3 := ((x)) => x; // fail + +} + +method Fail() { + var g8 := x : int => x; // not ok! +} + +function f():() { + a.b(x); a.b(x) +} + +method M() { + g := a.b(x); +} + +method M() { + g := y => a(y); +} + +method M() { + g := y => a.b(y); +} + +function f():() { + (u => a.b(x); a(x))(); a(x) +} diff --git a/Test/hofs/LambdaParsefail.dfy.expect b/Test/hofs/LambdaParsefail.dfy.expect new file mode 100644 index 00000000..b1334b85 --- /dev/null +++ b/Test/hofs/LambdaParsefail.dfy.expect @@ -0,0 +1,5 @@ +LambdaParsefail.dfy(5,17): error: Invalid variable binding in lambda. +LambdaParsefail.dfy(6,16): error: Expected variable binding. +LambdaParsefail.dfy(7,16): error: Expected variable binding. +LambdaParsefail.dfy(12,17): error: semi expected +4 parse errors detected in LambdaParsefail.dfy diff --git a/Test/hofs/LambdaParsefail2.dfy b/Test/hofs/LambdaParsefail2.dfy new file mode 100644 index 00000000..148fc03c --- /dev/null +++ b/Test/hofs/LambdaParsefail2.dfy @@ -0,0 +1,8 @@ +// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + + +method Fail2() { + var g4 := (x, y : A) => (y, x : B); // RHS should fail! +} + diff --git a/Test/hofs/LambdaParsefail2.dfy.expect b/Test/hofs/LambdaParsefail2.dfy.expect new file mode 100644 index 00000000..8bbf643c --- /dev/null +++ b/Test/hofs/LambdaParsefail2.dfy.expect @@ -0,0 +1,2 @@ +LambdaParsefail2.dfy(6,33): error: Type specification not allowed here, comma separator was expected. +1 parse errors detected in LambdaParsefail2.dfy diff --git a/Test/hofs/Map.dfy b/Test/hofs/Map.dfy new file mode 100644 index 00000000..a55be2be --- /dev/null +++ b/Test/hofs/Map.dfy @@ -0,0 +1,117 @@ + +datatype List = Nil | Cons(hd: A,tl: List); + +function method Map(f : A -> B, xs : List) : List + requires forall x :: f.requires(x); + reads *; + decreases xs; +{ + match xs + case Nil => Nil + case Cons(x,xs) => Cons(f(x),Map(f,xs)) +} + +function method Id(x : A) : A { x } + +method Test() { + assert Map(Id, Cons(1,Nil)) == Cons(1,Nil); + var inc := x => x + 1; + assert Map(inc, Cons(1,Nil)) == Cons(2,Nil); + assert Map(x => x + 1, Cons(1,Nil)) == Cons(2,Nil); + assert Map((x) requires x > 0 => x + 1, Nil) == Nil; +} + +function CanCall(f : A -> B, xs : List) : bool + decreases xs; + reads *; +{ + match xs + case Nil => true + case Cons(x,xs) => f.requires(x) && CanCall(f, xs) +} + +function method MegaMap(f : A -> B, xs : List) : List + requires CanCall(f, xs); + reads *; + decreases xs; +{ + match xs + case Nil => Nil + case Cons(x,xs) => Cons(f(x),MegaMap(f,xs)) +} + +method Test2() { + assert MegaMap((x) requires x != 0 => 100 / x, Cons(2, Nil)).hd == 50; +} + +function All(p : A -> bool, xs : List) : bool + requires forall x :: p.requires(x) /* && p.reads(x) == {} */; + reads *; + decreases xs; +{ + match xs + case Nil => true + case Cons(x,xs) => p(x) && All(p,xs) +} + +/* +function UnionMap(i : A -> set, ys : List): set + requires forall x :: i.requires(x) && i.reads(x) == {}; + decreases ys; +{ + match ys + case Nil => {} + case Cons(x,xs) => i(x) + UnionMap(i,xs) +} +*/ + +function method NinjaMap(f : A -> B, ys : List) : List + requires All(f.requires, ys); +// reads UnionMap(f.reads, ys); + reads *; + decreases ys; +{ + match ys + case Nil => Nil + case Cons(x,xs) => Cons(f(x),NinjaMap(f,xs)) +} + +function method Compose(f : B -> C, g : A -> B) : A -> C +{ + x requires g.requires(x) && f.requires(g(x)) + reads g.reads(x) + f.reads(g(x)) + => f(g(x)) +} + +lemma {:induction 0} MapCompose(f : B -> C, g : A -> B, xs : List) + requires All(g.requires, xs); + requires All(f.requires, NinjaMap(g,xs)); + requires All(Compose(f,g).requires, xs); + + decreases xs; + ensures NinjaMap(f,NinjaMap(g,xs)) == NinjaMap(Compose(f,g),xs); +{ + match xs + case Nil => + case Cons(x,xs) => + calc { + NinjaMap(f,NinjaMap(g,Cons(x,xs))); + == NinjaMap(f,Cons(g(x),NinjaMap(g,xs))); + == Cons(f(g(x)),NinjaMap(f,NinjaMap(g,xs))); + == { MapCompose(f,g,xs); } + Cons(f(g(x)),NinjaMap(Compose(f,g),xs)); + == Cons(Compose(f,g)(x),NinjaMap(Compose(f,g),xs)); + == NinjaMap(Compose(f,g),Cons(x,xs)); + } +} + +// auto-mode +lemma MapCompose2(f : B -> C, g : A -> B, xs : List) + requires All(g.requires, xs); + requires All(f.requires, NinjaMap(g,xs)); + requires All(Compose(f,g).requires, xs); + decreases xs; + ensures NinjaMap(f,NinjaMap(g,xs)) == NinjaMap(Compose(f,g),xs); +{ +} + diff --git a/Test/hofs/MutableField.dfy b/Test/hofs/MutableField.dfy new file mode 100644 index 00000000..fa0a1f50 --- /dev/null +++ b/Test/hofs/MutableField.dfy @@ -0,0 +1,15 @@ +// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + + +class C { + function method f(x : int) : int { x } + + var g : int -> int; + + method M() modifies this; + { + f := g; // not ok + } +} + diff --git a/Test/hofs/MutableField.dfy.expect b/Test/hofs/MutableField.dfy.expect new file mode 100644 index 00000000..1ffdc239 --- /dev/null +++ b/Test/hofs/MutableField.dfy.expect @@ -0,0 +1,2 @@ +MutableField.dfy(12,4): Error: LHS of assignment must denote a mutable field +1 resolution/type errors detected in MutableField.dfy diff --git a/Test/hofs/Naked.dfy b/Test/hofs/Naked.dfy new file mode 100644 index 00000000..17aa828a --- /dev/null +++ b/Test/hofs/Naked.dfy @@ -0,0 +1,51 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module Functions { + function f(x: nat): nat + { + if x == 0 then 0 else + if var b: bool :| true; b then + var h := f; + h(x-1) + else + (f)(x-1) + } + + function f1(x: nat): nat { if x == 0 then 0 else f2(x - 1) } + + function f2(x: nat): nat { if x == 0 then 0 else (f1)(x - 1) } +} + +module Requires { + function t(x: nat): nat + requires !t.requires(x); + { x } + + function g(x: nat): nat + requires !(g).requires(x); + { x } + + function g2(x: int): int { h(x) } + + function h(x: int): int + requires !g2.requires(x); + { x } +} + +module Reads { + function t(x: nat): nat + reads t.reads(x); + { x } + + function g(x: nat): nat + reads (g).reads(x); + { x } + + function g2(x: int): int { h(x) } + + function h(x: int): int + reads g2.reads(x); + { x } +} + diff --git a/Test/hofs/Naked.dfy.expect b/Test/hofs/Naked.dfy.expect new file mode 100644 index 00000000..62c035b2 --- /dev/null +++ b/Test/hofs/Naked.dfy.expect @@ -0,0 +1,50 @@ +Naked.dfy(9,16): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. +Execution trace: + (0,0): anon0 + (0,0): anon7_Else + (0,0): anon8_Else + (0,0): anon9_Then +Naked.dfy(12,8): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. +Execution trace: + (0,0): anon0 + (0,0): anon7_Else + (0,0): anon8_Else + (0,0): anon9_Else +Naked.dfy(17,53): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. +Execution trace: + (0,0): anon0 + (0,0): anon5_Else + (0,0): anon6_Else +Naked.dfy(22,13): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. +Execution trace: + (0,0): anon0 +Naked.dfy(26,14): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. +Execution trace: + (0,0): anon0 +Naked.dfy(29,30): Error: cannot prove termination; try supplying a decreases clause +Execution trace: + (0,0): anon0 + (0,0): anon3_Else +Naked.dfy(29,30): Error: possible violation of function precondition +Naked.dfy(32,14): Related location +Execution trace: + (0,0): anon0 + (0,0): anon3_Else +Naked.dfy(32,15): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. +Execution trace: + (0,0): anon0 +Naked.dfy(38,9): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. +Execution trace: + (0,0): anon0 +Naked.dfy(42,10): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. +Execution trace: + (0,0): anon0 +Naked.dfy(45,30): Error: cannot prove termination; try supplying a decreases clause +Execution trace: + (0,0): anon0 + (0,0): anon3_Else +Naked.dfy(48,11): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. +Execution trace: + (0,0): anon0 + +Dafny program verifier finished with 1 verified, 12 errors diff --git a/Test/hofs/OneShot.dfy b/Test/hofs/OneShot.dfy new file mode 100644 index 00000000..73b08fe2 --- /dev/null +++ b/Test/hofs/OneShot.dfy @@ -0,0 +1,25 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +class Ref { + var val : A; +} + +method OneShot() { + var g : () -> bool; + var i : Ref; + i := new Ref; + + g := () -> true; + + assert g(); + + i.val := i.val + 1; // heap changes + + if * { + assert g(); // should fail + } else { + assert !g(); // should fail + } +} + diff --git a/Test/hofs/OneShot.dfy.expect b/Test/hofs/OneShot.dfy.expect new file mode 100644 index 00000000..78a9864b --- /dev/null +++ b/Test/hofs/OneShot.dfy.expect @@ -0,0 +1,20 @@ +OneShot.dfy(20,12): Error: possible violation of function precondition +Execution trace: + (0,0): anon0 + (0,0): anon5_Then + OneShot.dfy(13,9): anon5_Else + (0,0): anon6_Then +OneShot.dfy(22,12): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon5_Then + OneShot.dfy(13,9): anon5_Else + (0,0): anon6_Else +OneShot.dfy(22,13): Error: possible violation of function precondition +Execution trace: + (0,0): anon0 + (0,0): anon5_Then + OneShot.dfy(13,9): anon5_Else + (0,0): anon6_Else + +Dafny program verifier finished with 1 verified, 3 errors diff --git a/Test/hofs/Quant.dfy b/Test/hofs/Quant.dfy new file mode 100644 index 00000000..70d15902 --- /dev/null +++ b/Test/hofs/Quant.dfy @@ -0,0 +1,132 @@ + +module QuantReads { + + function All(p : A -> bool) : bool + reads set x : A, y : object | y in p.reads(x) :: y; + requires forall x : A :: p.requires(x); + { + forall x : A :: p(x) + } + + lemma AllQuant(p : A -> bool) + requires All.requires(p); + requires All(p); + ensures forall x : A :: p(x); + { + } + +} + +module Forall { + + function All(p : A -> bool) : bool + { + forall x :: p.requires(x) && p(x) + } + + function CallMe(f : int -> int) : int + requires All(f.requires); + { + f(1) + f(2) + } + +} + +module Quant { + + function All(p : A -> bool) : bool + requires forall x : A :: p.requires(x); + { + forall x : A :: p(x) + } + + lemma AllBool(p : bool -> bool) + requires forall x : bool :: p.requires(x); + requires All(p); + ensures p(true) && p(false); + { + } + + method Boo() + requires All(x => x); + ensures false; + { + AllBool(x => x); + } + + lemma AllQuant(p : A -> bool) + requires All.requires(p); + requires All(p); + ensures forall x : A :: p(x); + { + } + + method Boo2() + requires All(x => x); + ensures false; + { + assert (x => x)(false); + } + + + method Koo(s : set, t : set) + requires All(x => (x in s ==> x in t) && (x in t ==> x in s)); + ensures All(x => x in s <==> x in t); + { + } + +} + +module ReadAll { + + datatype List = Nil | Cons(A,List); + + function All(p : A -> bool, xs : List) : bool + reads (set x, y | y in p.reads(x) :: y); + requires forall x :: p.reads(x) == {} && p.requires(x); + decreases xs; + { + match xs + case Nil => true + case Cons(x,xs) => p(x) && All(p,xs) + } + + function Div(xs : List) : List + requires All(x => x > 0, xs); + { + match xs + case Nil => Nil + case Cons(x,xs) => Cons(100 / x,Div(xs)) + } + +} + +module Requires { + + method SmallTest(f : int -> int) + requires f.requires(0); + { + print f(0); + } + + datatype List = Nil | Cons(hd: A,tl: List); + + function All(p : A -> bool, xs : List) : bool + requires forall x :: p.requires(x); + decreases xs; + { + match xs + case Nil => true + case Cons(x,xs) => p(x) && All(p,xs) + } + + function method Map(f : A -> B, ys : List) : List + requires All(f.requires, ys); + decreases ys; + { + match ys + case Nil => Nil + case Cons(x,xs) => Cons(f(x),Map(f,xs)) + } + +} diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy new file mode 100644 index 00000000..bc80713d --- /dev/null +++ b/Test/hofs/ReadsReads.dfy @@ -0,0 +1,59 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function MyReadsOk(f : A -> B, a : A) : set + reads f.reads(a); +{ + f.reads(a) +} + +function MyReadsOk2(f : A -> B, a : A) : set + reads f.reads(a); +{ + (f.reads)(a) +} + +function MyReadsOk3(f : A -> B, a : A) : set + reads (f.reads)(a); +{ + f.reads(a) +} + +function MyReadsOk4(f : A -> B, a : A) : set + reads (f.reads)(a); +{ + (f.reads)(a) +} + +function MyReadsBad(f : A -> B, a : A) : set +{ + f.reads(a) +} + +function MyReadsBad2(f : A -> B, a : A) : set +{ + (f.reads)(a) +} + +function MyReadsOk'(f : A -> B, a : A, o : object) : bool + reads f.reads(a); +{ + o in f.reads(a) +} + +function MyReadsBad'(f : A -> B, a : A, o : object) : bool +{ + o in f.reads(a) +} + +function MyRequiresOk(f : A -> B, a : A) : bool + reads f.reads(a); +{ + f.requires(a) +} + +function MyRequiresBad(f : A -> B, a : A) : bool +{ + f.requires(a) +} + diff --git a/Test/hofs/ReadsReads.dfy.expect b/Test/hofs/ReadsReads.dfy.expect new file mode 100644 index 00000000..50f74728 --- /dev/null +++ b/Test/hofs/ReadsReads.dfy.expect @@ -0,0 +1,18 @@ +ReadsReads.dfy(30,5): Error: insufficient reads clause to invoke function +Execution trace: + (0,0): anon0 + (0,0): anon3_Else +ReadsReads.dfy(35,3): Error: insufficient reads clause to invoke function +Execution trace: + (0,0): anon0 + (0,0): anon3_Else +ReadsReads.dfy(46,10): Error: insufficient reads clause to invoke function +Execution trace: + (0,0): anon0 + (0,0): anon3_Else +ReadsReads.dfy(57,5): Error: insufficient reads clause to invoke function +Execution trace: + (0,0): anon0 + (0,0): anon3_Else + +Dafny program verifier finished with 6 verified, 4 errors diff --git a/Test/hofs/Renaming.dfy b/Test/hofs/Renaming.dfy new file mode 100644 index 00000000..7a3f69a5 --- /dev/null +++ b/Test/hofs/Renaming.dfy @@ -0,0 +1,25 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function OnId(f : (bool -> bool) -> int) : int + reads f.reads(x => x); + requires f.requires(y => y); +{ + f(z => z) +} + +method Equal() { + var id1 : bool -> bool := x => x; + var id2 := y => y; + assert forall x :: id1(x) == id2(x); + assert id1 == id2; +} + +method K(P : (A -> A) -> bool) +{ + assume P.requires(x => x); + assume P(y => y); + assert P(z => z); + assert (x => y => x) == ((a : A) => (b : B) => a); +} + diff --git a/Test/hofs/Renaming.dfy.expect b/Test/hofs/Renaming.dfy.expect new file mode 100644 index 00000000..790f6509 --- /dev/null +++ b/Test/hofs/Renaming.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 5 verified, 0 errors diff --git a/Test/hofs/ResolveError.dfy b/Test/hofs/ResolveError.dfy new file mode 100644 index 00000000..7df4bbb3 --- /dev/null +++ b/Test/hofs/ResolveError.dfy @@ -0,0 +1,51 @@ +// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + + +method ResolutionErrors() { + var x; + var g5 := x, y => (y, x); // fail at resolution + var g6 := x, (y => (y, x)); // fail at resolution +} + +// cannot assign functions + +class Apa { + function f() : int { + 0 + } +} + +method Nope3() { + var apa := new Apa; + apa.f := () => 2; +} + +method RequiresFail(f : int -> int) + // ok + requires f(0) == 0; + requires f.requires(0); + requires f.reads(0) == {}; + + // fail + requires f(0) == true; + requires f(1,2) == 0; + requires f(true) == 0; + requires f.requires(true); + requires f.requires(1) == 0; + requires f.requires(1,2); + requires f.reads(true) == {}; + requires f.reads(1) == 0; + requires f.reads(1,2) == {}; +{ +} + +predicate method Bool() +{ + true +} + +method Bla() { + assert Bool; +} + diff --git a/Test/hofs/ResolveError.dfy.expect b/Test/hofs/ResolveError.dfy.expect new file mode 100644 index 00000000..acc01b73 --- /dev/null +++ b/Test/hofs/ResolveError.dfy.expect @@ -0,0 +1,14 @@ +ResolveError.dfy(7,11): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment +ResolveError.dfy(8,11): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment +ResolveError.dfy(21,6): Error: LHS of assignment must denote a mutable field +ResolveError.dfy(31,16): Error: arguments must have the same type (got int and bool) +ResolveError.dfy(32,12): Error: cannot apply arguments with types int,int to expression with type int -> int +ResolveError.dfy(33,12): Error: cannot apply arguments with types bool to expression with type int -> int +ResolveError.dfy(34,13): Error: incorrect type of function argument 0 (expected int, got bool) +ResolveError.dfy(35,25): Error: arguments must have the same type (got bool and int) +ResolveError.dfy(36,13): Error: wrong number of function arguments (got 2, expected 1) +ResolveError.dfy(37,13): Error: incorrect type of function argument 0 (expected int, got bool) +ResolveError.dfy(38,22): Error: arguments must have the same type (got set and int) +ResolveError.dfy(39,13): Error: wrong number of function arguments (got 2, expected 1) +ResolveError.dfy(49,9): Error: condition is expected to be of type bool, but is () -> bool +13 resolution/type errors detected in ResolveError.dfy diff --git a/Test/hofs/Simple.dfy b/Test/hofs/Simple.dfy new file mode 100644 index 00000000..4bb58078 --- /dev/null +++ b/Test/hofs/Simple.dfy @@ -0,0 +1,90 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function method MkId() : A -> A { + x => x +} + +function method IntId() : int -> int { + y => y +} + +function method DivZero() : int -> int +{ + z => 5 / z // div by zero +} + +function method DivZeroWithReq() : int -> int +{ + (z) requires z != 0 => 5 / z +} + +function method DivZero2() : (int, int) -> int { + (x, y) requires y != 0 => x / y +} + +function method DivZero3() : int -> int { + z => z / 0 // div by zero +} + +function method Shadow() : int -> real -> real { + x => x => x +} + +method Reqs() { + var fn := (u) requires u => u; + print fn(true); + print fn(false); // precond violation +} + +method Main() { + var id := IntId(); + print id(5); + var polyid : int -> int := MkId(); + print polyid(5); + assert id(2) == polyid(2); + assert id(3) != 4 && 5 != polyid(6); + var divvy := DivZero2(); + print divvy(2,5); + print divvy(2,0); // precond violation +} + +function method succ(x : int) : int + requires x > 0; +{ + x + 1 +} + +method Main2() { + var suc := succ; + assert suc(3) == succ(3); + assert suc(-1) == 0; // precond violation +} + +function method Id(x : A) : A { + x +} + + +method Main3() { + var id := Id; + assert id(3) == 3; + assert forall x :: (Id(id))(x) == (y => y)(x); + assert forall x :: (Id(id))(x) == (y => y)(2); // should fail +} + + +function P(f: A -> B, x : A): B + reads (f.reads)(x); + requires (f.requires)(x); +{ + f(x) +} + +function Q(f: U -> V, x : U): V + reads (f.reads)(x); // would be nice to be able to write P.reads(f,x) + requires (f.requires)(x); +{ + P(f,x) +} + diff --git a/Test/hofs/Simple.dfy.expect b/Test/hofs/Simple.dfy.expect new file mode 100644 index 00000000..76871e06 --- /dev/null +++ b/Test/hofs/Simple.dfy.expect @@ -0,0 +1,32 @@ +Simple.dfy(14,10): Error: possible division by zero +Execution trace: + (0,0): anon0 + (0,0): anon5_Else + (0,0): anon6_Then +Simple.dfy(27,10): Error: possible division by zero +Execution trace: + (0,0): anon0 + (0,0): anon5_Else + (0,0): anon6_Then +Simple.dfy(37,9): Error: possible violation of function precondition +Execution trace: + (0,0): anon0 + Simple.dfy(35,15): anon5_Else +Simple.dfy(49,9): Error: possible violation of function precondition +Execution trace: + (0,0): anon0 + (0,0): anon3_Then + (0,0): anon2 +Simple.dfy(61,10): Error: possible violation of function precondition +Execution trace: + (0,0): anon0 +Simple.dfy(61,18): Error: assertion violation +Execution trace: + (0,0): anon0 +Simple.dfy(73,10): Error: assertion violation +Execution trace: + (0,0): anon0 + Simple.dfy(72,38): anon5_Else + Simple.dfy(73,38): anon6_Else + +Dafny program verifier finished with 13 verified, 7 errors diff --git a/Test/hofs/TreeMap.dfy b/Test/hofs/TreeMap.dfy new file mode 100644 index 00000000..95b07590 --- /dev/null +++ b/Test/hofs/TreeMap.dfy @@ -0,0 +1,215 @@ + +datatype List = Nil | Cons(head: A,tail: List); + +datatype Tree = Branch(val: A,trees: List>); + +function Set(xs : List) : set + ensures forall x :: x in Set(xs) ==> x < xs; +{ + match xs + case Nil => {} + case Cons(x,xs) => {x} + Set(xs) +} + +function TSet(t0 : Tree) : set + ensures forall t :: t in TSet(t0) ==> t < t0; +{ + match t0 case Branch(x,ts) => {x} + set t, y | t in Set(ts) && y in TSet(t) :: y +} + +// reads {} + +function ReadNothingMap(f : A -> B, xs: List): List + requires forall x :: x in Set(xs) ==> f.requires(x); + requires forall x :: f.reads(x) == {}; + decreases xs; +{ + match xs + case Nil => Nil + case Cons(x,xs) => Cons(f(x),ReadNothingMap(f,xs)) +} + +function TReadNothingMap(f: A -> B, t0: Tree): Tree + requires forall x {:heapQuantifier} :: f.requires(x); + requires forall x {:heapQuantifier} :: f.reads(x) == {}; + decreases t0; +{ + var Branch(x,ts) := t0; + Branch(f(x), ReadNothingMap(t requires t in Set(ts) => TReadNothingMap(f,t), ts)) +} + +function TReadNothingMap2(f: A -> B, t0: Tree): Tree + requires forall x :: f.requires(x); + requires forall x :: f.reads(x) == {}; + decreases t0; +{ + var Branch(x,ts) := t0; + Branch(f(x), ReadNothingMap(t requires t in Set(ts) -> TReadNothingMap2(f,t), ts)) +} + +function TReadNothingMap3(f: A -> B, t0: Tree): Tree + requires forall x :: f.requires(x); + requires forall x :: f.reads(x) == {}; + decreases t0; +{ + var Branch(x,ts) := t0; + Branch(f(x), ReadNothingMap( + t requires t in Set(ts) + requires (forall x :: x in TSet(t) ==> f.requires(x)) + => TReadNothingMap(f,t), ts)) +} + +method TestReadNothingStar() { + assert TReadNothingMap(x => x + 1, Branch(1,Nil)).Branch?; + + assert TReadNothingMap(x => x + 1, Branch(0,Nil)) == Branch(1,Nil); + + assert TReadNothingMap(x => x + 1, Branch(1,Cons(Branch(0,Nil),Nil))) + == Branch(2,Cons(Branch(1,Nil),Nil)); + + assert TReadNothingMap2(x -> x + 1, Branch(1,Nil)).Branch?; + + assert TReadNothingMap2(x -> x + 1, Branch(0,Nil)) == Branch(1,Nil); + + assert TReadNothingMap2(x -> x + 1, Branch(1,Cons(Branch(0,Nil),Nil))) + == Branch(2,Cons(Branch(1,Nil),Nil)); +} + +/// reads * + +function ReadStarMap(f : A -> B, xs: List): List + requires forall x :: x in Set(xs) ==> f.requires(x); + reads *; + decreases xs; +{ + match xs + case Nil => Nil + case Cons(x,xs) => Cons(f(x),ReadStarMap(f,xs)) +} + +function TReadStarMap(f: A -> B, t0: Tree): Tree + requires forall x {:heapQuantifier} :: f.requires(x); + reads *; + decreases t0; +{ + var Branch(x,ts) := t0; + Branch(f(x), ReadStarMap(t reads * requires t in Set(ts) => TReadStarMap(f,t), ts)) +} + +function TReadStarMap2(f: A -> B, t0: Tree): Tree + requires forall x :: f.requires(x); + reads *; + decreases t0; +{ + var Branch(x,ts) := t0; + Branch(f(x), ReadStarMap(t reads * requires t in Set(ts) -> TReadStarMap2(f,t), ts)) +} + +lemma LitTReadStarMap2(f : A -> B, x : A, ts: List>) + requires forall u :: f.requires(u); + ensures TReadStarMap2(f, Branch(x,ts)) == + Branch(f(x), ReadStarMap(t reads * requires t in Set(ts) -> TReadStarMap2(f,t), ts)); +{ + assert TReadStarMap2(f, Branch(x,ts)).val == f(x); + if (ts.Nil?) { + assert TReadStarMap2(f, Branch(x,ts)).trees == + ReadStarMap(t reads * requires t in Set(ts) -> TReadStarMap2(f,t),ts); + } else { + assert TReadStarMap2(f, Branch(x,ts)).trees == + ReadStarMap(t reads * requires t in Set(ts) -> TReadStarMap2(f,t),ts); + } +} + +method TestReadStar() { + assert TReadStarMap(x => x + 1, Branch(1,Nil)).Branch?; + + assert TReadStarMap(x => x + 1, Branch(0,Nil)) == Branch(1,Nil); + + assert ReadStarMap(t reads * requires t in Set(Cons(Branch(0,Nil),Nil)) -> TReadStarMap(x => x + 1,t) + , Cons(Branch(0,Nil),Nil)) + == Cons(Branch(1,Nil),Nil); + + assert TReadStarMap(x => x + 1, Branch(1,Cons(Branch(0,Nil),Nil))).Branch?; + + assert TReadStarMap(x => x + 1, Branch(1,Cons(Branch(0,Nil),Nil))).val == 2; + + assert TReadStarMap(x => x + 1, Branch(1,Cons(Branch(0,Nil),Nil))).trees == Cons(Branch(1,Nil),Nil); + + assert TReadStarMap(x => x + 1, Branch(1,Cons(Branch(0,Nil),Nil))) + == Branch(2,Cons(Branch(1,Nil),Nil)); + + assert TReadStarMap2(x -> x + 1, Branch(1,Nil)).Branch?; + + assert TReadStarMap2(x -> x + 1, Branch(0,Nil)) == Branch(1,Nil); + + assert TReadStarMap2(x -> x + 1, Branch(1,Cons(Branch(0,Nil),Nil))) + == Branch(2,Cons(Branch(1,Nil),Nil)); +} + +/// reads exact + +function Map(f : A -> B, xs: List): List + requires forall x :: x in Set(xs) ==> f.requires(x); + reads set x, y | x in Set(xs) && y in f.reads(x) :: y; + decreases xs; +{ + match xs + case Nil => Nil + case Cons(x,xs) => Cons(f(x),Map(f,xs)) +} + +function TMap(f : A -> B, t0: Tree): Tree + requires forall t :: t in TSet(t0) ==> f.requires(t); + reads set x, y | x in TSet(t0) && y in f.reads(x) :: y; + decreases t0; +{ + var Branch(x,ts) := t0; + Branch( + f(x), + Map( t requires t in Set(ts) + reads set x, y | x in TSet(t) && y in f.reads(x) :: y + -> TMap(f,t) + , ts) + ) +} + +lemma LitTMap(f : A -> B,x : A, ts: List>) + requires f.requires(x); + requires forall t, u :: t in Set(ts) && u in TSet(t) ==> f.requires(u); + ensures TMap(f, Branch(x,ts)) == + Branch(f(x), + Map( t requires t in Set(ts) + reads set x, y | x in TSet(t) && y in f.reads(x) :: y + -> TMap(f,t),ts)); +{ + assert TMap(f, Branch(x,ts)).val == f(x); + assert TMap(f, Branch(x,ts)).trees == + Map(t requires t in Set(ts) + reads set x, y | x in TSet(t) && y in f.reads(x) :: y + -> TMap(f,t),ts); +} + +method Test() { + assert TMap(x -> x + 1, Branch(1,Nil)).Branch?; + + assert TMap(x -> x + 1, Branch(0,Nil)) == Branch(1,Nil); + + calc { + TMap(x -> x + 1, Branch(1,Cons(Branch(0,Nil),Nil))); + == { LitTMap(x -> x + 1,1, Cons(Branch(0,Nil),Nil)); } + Branch((x -> x + 1)(1),Map(t -> TMap(x -> x + 1,t),Cons(Branch(0,Nil),Nil))); + == + Branch(2,Map(t -> TMap(x -> x + 1,t),Cons(Branch(0,Nil),Nil))); + == + Branch(2,Map(t -> TMap(x -> x + 1,t),Cons(Branch(0,Nil),Nil))); + == + Branch(2,Cons(TMap(x -> x + 1,Branch(0,Nil)),Nil)); + == + Branch(2,Cons(Branch((x -> x + 1)(0),Nil),Nil)); + == + Branch(2,Cons(Branch(1,Nil),Nil)); + } + + assert TMap(x -> x + 1, Branch(1,Cons(Branch(0,Nil),Nil))) + == Branch(2,Cons(Branch(1,Nil),Nil)); +} diff --git a/Test/hofs/TreeMapSimple.dfy b/Test/hofs/TreeMapSimple.dfy new file mode 100644 index 00000000..3ba4ffd6 --- /dev/null +++ b/Test/hofs/TreeMapSimple.dfy @@ -0,0 +1,49 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +datatype List = Nil | Cons(head: A,tail: List); + +datatype Tree = Branch(val: A,trees: List>); + +function ListData(xs : List) : set + ensures forall x :: x in ListData(xs) ==> x < xs; +{ + match xs + case Nil => {} + case Cons(x,xs) => {x} + ListData(xs) +} + +function TreeData(t0 : Tree) : set + ensures forall t :: t in TreeData(t0) ==> t < t0; +{ + var Branch(x,ts) := t0; + {x} + set t, y | t in ListData(ts) && y in TreeData(t) :: y +} + +function Pre(f : A -> B, s : set) : bool + reads (set x, y | x in s && y in f.reads(x) :: y); +{ + forall x :: x in s ==> f.reads(x) == {} && f.requires(x) +} + +function method Map(xs : List, f : A -> B): List + reads (set x, y | x in ListData(xs) && y in f.reads(x) :: y); + requires Pre(f, ListData(xs)); + decreases xs; +{ + match xs + case Nil => Nil + case Cons(x,xs) => Cons(f(x),Map(xs,f)) +} + +function method TMap(t0 : Tree, f : A -> B) : Tree + reads (set x, y | x in TreeData(t0) && y in f.reads(x) :: y); + requires Pre(f, TreeData(t0)); + decreases t0; +{ + var Branch(x,ts) := t0; + Branch(f(x),Map(ts, t requires t in ListData(ts) + requires Pre(f, TreeData(t)) + => TMap(t,f))) +} + diff --git a/Test/hofs/TreeMapSimple.dfy.expect b/Test/hofs/TreeMapSimple.dfy.expect new file mode 100644 index 00000000..790f6509 --- /dev/null +++ b/Test/hofs/TreeMapSimple.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 5 verified, 0 errors diff --git a/Test/hofs/Twice.dfy b/Test/hofs/Twice.dfy new file mode 100644 index 00000000..2178db9f --- /dev/null +++ b/Test/hofs/Twice.dfy @@ -0,0 +1,38 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function method Twice(f : A -> A): A -> A +{ + x requires f.requires(x) && f.requires(f(x)) + reads f.reads(x) reads if f.requires(x) then f.reads(f(x)) else {} + => f(f(x)) +} + +method Simple() { + assert Twice(x => x + 1)(0) == 2; + assert Twice(Twice(x => x + 1))(0) == 4; + + // why does these fail? need requires/reads for literals? + // assert Twice(Twice)(x => x + 1)(0) == 4; + // assert Twice(Twice)(Twice)(x => x + 1)(0) == 16; +} + +method WithReads() { + var a : array := new int[1]; + a[0] := 1; + var f := x reads a => x + a[0]; + assert Twice(f)(0) == 2; + a[0] := 2; + assert Twice(f)(0) == 4; + assert Twice(f)(0) == 2; // should fail + assert false; // should fail +} + + +function method Twice_bad(f : A -> A): A -> A +{ + x requires f.requires(x) && f.requires(f(x)) + reads f.reads(x) + f.reads(f(x)) + => f(f(x)) +} + diff --git a/Test/hofs/Twice.dfy.expect b/Test/hofs/Twice.dfy.expect new file mode 100644 index 00000000..5ba4b47b --- /dev/null +++ b/Test/hofs/Twice.dfy.expect @@ -0,0 +1,11 @@ +Twice.dfy(27,22): Error: assertion violation +Execution trace: + (0,0): anon0 + Twice.dfy(23,12): anon3_Else +Twice.dfy(35,32): Error: possible violation of function precondition +Execution trace: + (0,0): anon0 + (0,0): anon9_Else + (0,0): anon10_Then + +Dafny program verifier finished with 4 verified, 2 errors diff --git a/Test/hofs/Types.dfy b/Test/hofs/Types.dfy new file mode 100644 index 00000000..9f62763a --- /dev/null +++ b/Test/hofs/Types.dfy @@ -0,0 +1,20 @@ +// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +method FnEqGhost() { + ghost var f : A -> A -> A; + ghost var g : A -> (A -> A); + ghost var h : (A -> A) -> A; + ghost var b1 := f == g; // type checking should be ok + ghost var b2 := f == h; // type checking should fail + + ghost var z; + ghost var b3 := f == z; // unify in progress + ghost var b4 := g == z; // should now be ok + ghost var b5 := h == z; // should now fail + + ghost var zz; + ghost var b6 := h == zz; // unify in progress + ghost var b7 := g == zz; // should fail +} + diff --git a/Test/hofs/Types.dfy.expect b/Test/hofs/Types.dfy.expect new file mode 100644 index 00000000..11d74db0 --- /dev/null +++ b/Test/hofs/Types.dfy.expect @@ -0,0 +1,4 @@ +Types.dfy(9,20): Error: arguments must have the same type (got A -> A -> A and (A -> A) -> A) +Types.dfy(14,20): Error: arguments must have the same type (got (A -> A) -> A and A -> A -> A) +Types.dfy(18,20): Error: arguments must have the same type (got A -> A -> A and (A -> A) -> A) +3 resolution/type errors detected in Types.dfy diff --git a/Test/hofs/WhileLoop.dfy b/Test/hofs/WhileLoop.dfy new file mode 100644 index 00000000..dd95cc76 --- /dev/null +++ b/Test/hofs/WhileLoop.dfy @@ -0,0 +1,50 @@ +// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +class Ref { + var val: A; +} + +method Nice(n: int) { + var f : int -> int := x => x; + var i := new Ref; + i.val := 0; + while (i.val < n) + invariant forall u :: f.requires(u); + invariant forall u :: f.reads(u) == {}; + invariant forall u :: f(u) == u + i.val; + { + i.val := i.val + 1; + f := x => f(x) + 1; + } +} + + +method OneShot(n: int) { + var f : int -> int := x => x; + var i := 0; + while (i < n) + invariant forall u :: f.requires(u); + invariant forall u :: f(u) == u + i; + { + i := i + 1; + f := x reads f.reads(x) -> f(x) + 1; + } +} + +method HeapQuant(n: int) { + var f : int -> int := x => x; + var i := new Ref; + ghost var r := 0; + i.val := 0; + while (i.val < n) + invariant forall u {:heapQuantifier} :: f.requires(u); + invariant forall u {:heapQuantifier} :: f.reads(u) == {}; + invariant r == i.val; + invariant forall u {:heapQuantifier} :: f(u) == u + r; + { + i.val, r := i.val + 1, r + 1; + f := x => f(x) + 1; + } +} + diff --git a/Test/hofs/WhileLoop.dfy.expect b/Test/hofs/WhileLoop.dfy.expect new file mode 100644 index 00000000..4ef2de53 --- /dev/null +++ b/Test/hofs/WhileLoop.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 6 verified, 0 errors -- cgit v1.2.3