diff options
| author |  stefanheule <unknown> | 2011-07-20 09:09:29 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2011-07-20 09:09:29 +0200 |
| commit | 3c444fc12ae2bba9c803631d521e37d49d741c35 (patch) | |
| tree | c67f652f736a5ba48412795561c5c3b46e184adc /Chalice | |
| parent | 4d833ac1672910e88ab2f9be6dbf7cad98195300 (diff) | |
Chalice: Uniform usage of Boogie syntax for functions.
Diffstat (limited to 'Chalice')
| -rw-r--r-- | Chalice/src/Prelude.scala | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Chalice/src/Prelude.scala b/Chalice/src/Prelude.scala index f4a99796..62597e8e 100644 --- a/Chalice/src/Prelude.scala +++ b/Chalice/src/Prelude.scala @@ -106,7 +106,7 @@ axiom Permission$denominator == 100000000000;""" }
object PercentageFunctionPL extends PreludeComponent {
val text = """
-function Fractions(n: int): int
+function Fractions(n: int) returns (int)
{
n * Permission$denominator
}
@@ -120,8 +120,8 @@ axiom predicateK == channelK && channelK == monitorK;""" }
object PercentageUninterpretedFunctionPL extends PreludeComponent {
val text = """
-function Fractions(n: int): int;
-function Fractions'(n: int): int;
+function Fractions(n: int) returns (int);
+function Fractions'(n: int) returns (int);
axiom (forall x: int :: { Fractions(x) } Fractions(x) == Fractions'(x));
axiom (forall x,y: int :: 0 <= x && x <= y ==> Fractions'(x) <= Fractions'(y));
axiom (forall x,y: int :: { Fractions(x), Fractions(y) } Fractions(x) + Fractions(y) == Fractions'(x+y));
|