forked from epfl-lara/stainless
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
BigInt instead of Int, to prevent princess OOM in ensures test. Facto…
…red out Forall and Ensures Vk/princessbigint (epfl-lara#1569) * BigInt instead of Int, to prevent princess OOM in ensures test * Factored ensures and Forall out of stainless.lang * Removed unnecessary own-package-import * Update libfiles.txt --------- Co-authored-by: Mario Bucev <[email protected]>
- Loading branch information
1 parent
21d0974
commit 4c65b07
Showing
5 changed files
with
123 additions
and
111 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,67 @@ | ||
| package stainless.lang | ||
| import stainless.annotation.* | ||
|
|
||
| object Ensures { | ||
| /* `ensures` is an `ensuring` property for first-class functions. */ | ||
|
|
||
| // For performance, we hide forall with @opaque | ||
| @ghost @opaque @library | ||
| def ensures[A,B](f: A => B, post: (A, B) => Boolean): Boolean = { | ||
| forall[A]((a: A) => post(a, f(a))) | ||
| } | ||
|
|
||
| // We instantiate it explicitly with `ensuresOf` on a given argument | ||
| @ghost @opaque @library | ||
| def ensuresOf[A,B](f: A => B, post: (A, B) => Boolean)(a: A): Unit = { | ||
| require(ensures(f, post)) | ||
| unfold(ensures(f,post)) | ||
| }.ensuring(_ => post(a, f(a))) | ||
|
|
||
| /* To establish ensures(f,post), create a function with this as postcondition and unfold | ||
| the ensures, e.g. | ||
| @ghost @opaque | ||
| def incIncreasing: Unit = { | ||
| unfold(ensures(inc, increasing)) | ||
| }.ensuring(_ => ensures(inc, increasing)) | ||
| */ | ||
|
|
||
| // Larger arities | ||
|
|
||
| @ghost @opaque @library | ||
| def ensures2[A1,A2,B](f: (A1,A2) => B, post: (A1, A2, B) => Boolean): Boolean = { | ||
| forall[A1,A2]((a1: A1, a2: A2) => post(a1, a2, f(a1,a2))) | ||
| } | ||
| @ghost @opaque @library | ||
| def ensures2of[A1,A2,B](f: (A1,A2) => B, post: (A1, A2, B) => Boolean)(a1: A1, a2: A2): Unit = { | ||
| require(ensures2[A1,A2,B](f, post)) | ||
| unfold(ensures2[A1,A2,B](f,post)) | ||
| }.ensuring(_ => post(a1, a2, f(a1,a2))) | ||
|
|
||
| @ghost @opaque @library | ||
| def ensures3[A1,A2,A3,B](f: (A1,A2,A3) => B, | ||
| post: (A1, A2, A3, B) => Boolean): Boolean = { | ||
| forall[A1,A2,A3]((a1: A1, a2: A2, a3: A3) => post(a1, a2, a3, f(a1,a2,a3))) | ||
| } | ||
| @ghost @opaque @library | ||
| def ensures3of[A1,A2,A3,B](f: (A1,A2,A3) => B, post: (A1, A2, A3, B) => Boolean) | ||
| (a1: A1, a2: A2, a3: A3): Unit = { | ||
| require(ensures3(f, post)) | ||
| unfold(ensures3(f,post)) | ||
| }.ensuring(_ => post(a1, a2, a3, f(a1,a2,a3))) | ||
|
|
||
| @ghost @opaque @library | ||
| def ensures4[A1,A2,A3,A4,B](f: (A1,A2,A3,A4) => B, | ||
| post: (A1, A2, A3, A4, B) => Boolean): Boolean = { | ||
| forall[A1,A2,A3,A4]((a1: A1, a2: A2, a3: A3, a4: A4) => post(a1, a2, a3, a4, f(a1,a2,a3,a4))) | ||
| } | ||
| @ghost @opaque @library | ||
| def ensures4of[A1,A2,A3,A4,B](f: (A1,A2,A3,A4) => B, | ||
| post: (A1, A2, A3, A4, B) => Boolean) | ||
| (a1: A1, a2: A2, a3: A3, a4: A4): Unit = { | ||
| require(ensures4(f, post)) | ||
| unfold(ensures4(f,post)) | ||
| }.ensuring(_ => post(a1, a2, a3, a4, f(a1,a2,a3,a4))) | ||
|
|
||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,45 @@ | ||
| package stainless.lang | ||
| import stainless.annotation.* | ||
| object Forall { | ||
| // Forall is opaque forall with (numbers in name instead of overloading) | ||
| @ghost @opaque @library | ||
| def Forall[A](p: A => Boolean): Boolean = forall(p) | ||
| @ghost @opaque @library | ||
| def Forall2[A,B](p: (A,B) => Boolean): Boolean = forall(p) | ||
| @ghost @opaque @library | ||
| def Forall3[A,B,C](p: (A,B,C) => Boolean): Boolean = forall(p) | ||
| @ghost @opaque @library | ||
| def Forall4[A,B,C,D](p: (A,B,C,D) => Boolean): Boolean = forall(p) | ||
| @ghost @opaque @library | ||
| def Forall5[A,B,C,D,E](p: (A,B,C,D,E) => Boolean): Boolean = forall(p) | ||
|
|
||
| // We instantiate it explicitly. | ||
| @ghost @opaque @library | ||
| def ForallOf[A](p: A => Boolean)(a: A): Unit = { | ||
| require(Forall(p)) | ||
| unfold(Forall(p)) | ||
| }.ensuring(_ => p(a)) | ||
|
|
||
| // Predicates of larger arity | ||
| @ghost @opaque @library | ||
| def Forall2of[A,B](p: (A,B) => Boolean)(a: A, b: B): Unit = { | ||
| require(Forall2(p)) | ||
| unfold(Forall2(p)) | ||
| }.ensuring(_ => p(a,b)) | ||
| @ghost @opaque @library | ||
| def Forall3of[A,B,C](p: (A,B,C) => Boolean)(a: A, b: B, c: C): Unit = { | ||
| require(Forall3(p)) | ||
| unfold(Forall3(p)) | ||
| }.ensuring(_ => p(a,b,c)) | ||
| @ghost @opaque @library | ||
| def Forall4of[A,B,C,D](p: (A,B,C,D) => Boolean)(a: A, b: B, c: C, d: D): Unit = { | ||
| require(Forall4(p)) | ||
| unfold(Forall4(p)) | ||
| }.ensuring(_ => p(a,b,c,d)) | ||
| @ghost @opaque @library | ||
| def Forall5of[A,B,C,D,E](p: (A,B,C,D,E) => Boolean)(a: A, b: B, c: C, d: D, e: E): Unit = { | ||
| require(Forall5(p)) | ||
| unfold(Forall5(p)) | ||
| }.ensuring(_ => p(a,b,c,d,e)) | ||
|
|
||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters