From 32effe3867360e4f10214be12f2b3f35db929f8b Mon Sep 17 00:00:00 2001 From: Dan Rosén Date: Wed, 13 Aug 2014 09:05:25 -0700 Subject: Add lambda compilation example, and remove some unused files from the tests --- Test/hofs/Compilation.dfy | 2 + Test/hofs/Compilation.dfy.expect | 19 +++- Test/hofs/Map.dfy | 117 --------------------- Test/hofs/Quant.dfy | 132 ------------------------ Test/hofs/TreeMap.dfy | 215 --------------------------------------- 5 files changed, 20 insertions(+), 465 deletions(-) delete mode 100644 Test/hofs/Map.dfy delete mode 100644 Test/hofs/Quant.dfy delete mode 100644 Test/hofs/TreeMap.dfy (limited to 'Test/hofs') diff --git a/Test/hofs/Compilation.dfy b/Test/hofs/Compilation.dfy index c3132db2..2033dabf 100644 --- a/Test/hofs/Compilation.dfy +++ b/Test/hofs/Compilation.dfy @@ -1,3 +1,5 @@ +// RUN: %dafny /compile:3 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" class Ref { var val : A; diff --git a/Test/hofs/Compilation.dfy.expect b/Test/hofs/Compilation.dfy.expect index 0c6452d2..06c13679 100644 --- a/Test/hofs/Compilation.dfy.expect +++ b/Test/hofs/Compilation.dfy.expect @@ -1,3 +1,20 @@ Dafny program verifier finished with 2 verified, 0 errors -Compiled assembly into Compilation.exe +Program compiled successfully +Running... + +1 = 1 +3 = 3 +3 = 3 +0 = 0 +3 = 3 +4 = 4 +3 = 3 +4 = 4 +3 = 3 +4 = 4 +4 = 4 +5 = 5 +55 = 55 +0 = 0 +1 = 1 diff --git a/Test/hofs/Map.dfy b/Test/hofs/Map.dfy deleted file mode 100644 index a55be2be..00000000 --- a/Test/hofs/Map.dfy +++ /dev/null @@ -1,117 +0,0 @@ - -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/Quant.dfy b/Test/hofs/Quant.dfy deleted file mode 100644 index 70d15902..00000000 --- a/Test/hofs/Quant.dfy +++ /dev/null @@ -1,132 +0,0 @@ - -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/TreeMap.dfy b/Test/hofs/TreeMap.dfy deleted file mode 100644 index 95b07590..00000000 --- a/Test/hofs/TreeMap.dfy +++ /dev/null @@ -1,215 +0,0 @@ - -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)); -} -- cgit v1.2.3