diff options
| author |  Nada Amin <namin@alum.mit.edu> | 2014-03-12 15:18:50 +0100 |
|---|---|---|
| committer | Nada Amin <namin@alum.mit.edu> | 2014-03-12 15:18:50 +0100 |
| commit | 4d43b6bccb7a8089011696c85c2d505dedb857ab (patch) | |
| tree | 2d8a2c802f8c324c3a820aae932970aed7a1fbec /Test/dafny0/Computations.dfy | |
| parent | 4e5238a39ae6c01b3b465d415c7a58c7d29b073c (diff) | |
Improve computations, in particular compositionality. Isolated useless literals around if-then-else as a surprising source of practical hanging.
Diffstat (limited to 'Test/dafny0/Computations.dfy')
| -rw-r--r-- | Test/dafny0/Computations.dfy | 19 |
1 files changed, 6 insertions, 13 deletions
diff --git a/Test/dafny0/Computations.dfy b/Test/dafny0/Computations.dfy index 4b975559..d3c42af5 100644 --- a/Test/dafny0/Computations.dfy +++ b/Test/dafny0/Computations.dfy @@ -151,19 +151,12 @@ ghost method copt_test() {
}
-// The following is a test that well-typedness antecednets are included in the literal axioms
-static function StaticFact(n: nat): nat
- ensures 0 < StaticFact(n);
+function power(b: int, n: nat): int
{
- if n == 0 then 1 else n * StaticFact(n - 1)
+ if (n==0) then 1 else b*power(b, n-1)
}
-static method test_StaticFact()
-{
- assert StaticFact(0) == 1;
- assert 42 != 42; // error: this should fail
-}
-method test_fact()
+
+ghost method test_power()
+ ensures power(power(2, 3), 1+power(2, 2))==32768;
{
- assert fact(0) == 1;
- assert 42 != 42; // error: this should fail
-}
+}
\ No newline at end of file |