You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: Guidelines.md
+10-2Lines changed: 10 additions & 2 deletions
Original file line number
Diff line number
Diff line change
@@ -1,4 +1,8 @@
1
-
Following are guidelines that one should follow unless there is a good technical reason not to.
1
+
The Dafny 386 guidelines.
2
+
3
+
By default, you should adhere the following guidelines to structure your development.
4
+
It may happen that not following the guidelines would lead to a better solution: when that is
5
+
the case, you should present your case with the rest of the developers.
2
6
3
7
* Languages features to avoid:
4
8
* import opened.
@@ -8,10 +12,13 @@ Following are guidelines that one should follow unless there is a good technical
8
12
9
13
* Even if a function is not meant to be part of the compiled code, don't use ghost unless necessary.
10
14
* Do not attach postconditions to functions. Instead, prove the postcondition as a separate lemma.
15
+
* Use function preconditions only when the function is genuinely partial and that making total would requires the use of the error monad or a dummy value.
11
16
* Make functions opaque.
12
17
* Name preconditions of lemmas and reveal them only when necessary.
13
18
* Be mindful of resource usage and refine your proof until it is less than 1M.
14
-
* In particular, avoid `{:vcs_split_on_every_assert}` as this can increase the verification time a lot.
19
+
* Do not use internal prover directives such as `{:vcs_split_on_every_assert}` or `{:trigger}`.
20
+
* A method should have a unique postcondition that establishes its equivalence with a functional model.
21
+
* Local variables must be typed explicitly.
15
22
* Keep proofs short and modular, as for a pencil and paper proof.
16
23
* Prefer structured proofs in natural deduction rathen than sequences of assertions.
17
24
* Unless it is logically or mathematically necessary:
@@ -143,6 +150,7 @@ lemma Foo2()
143
150
</td>
144
151
</tr>
145
152
</table>
153
+
146
154
* Establish preconditions of assertion in a by clause. For example, consider lemma Foo() requires A ensures B
Copy file name to clipboardExpand all lines: docs/dafny/ExamplesExternUniform.dfy
+10-32Lines changed: 10 additions & 32 deletions
Original file line number
Diff line number
Diff line change
@@ -8,6 +8,7 @@
8
8
include "../../src/Dafny-VMC.dfy"
9
9
10
10
module RandomExamples {
11
+
import Rationals
11
12
import DafnyVMC
12
13
13
14
methodMain()
@@ -55,62 +56,39 @@ module RandomExamples {
55
56
}
56
57
print "Estimated probabilities for UniformInterval(7,10): ", (a asreal) / (n asreal), "; ", (b asreal) / (n asreal), "; " , (c asreal) / (n asreal), " (each should be around 0.33)\n";
57
58
58
-
a := 0;
59
-
b := 0;
60
-
for i := 0 to n {
61
-
var k := r.Geometric();
62
-
if k == 5 {
63
-
a := a + 1;
64
-
} elseif k == 10 {
65
-
b := b + 1;
66
-
}
67
-
}
68
-
print "Estimated probabilities for Geometric(0.5): " , (a asreal) / (n asreal), " (should be around 0.015625) and " , (b asreal) / (n asreal), " (should be around 0.00048828125) \n";
69
-
70
59
t := 0;
71
60
for i := 0 to n {
72
-
var b := r.BernoulliRational(1, 5);
61
+
var b := r.Bernoulli(Rationals.Rational(1, 5));
73
62
if b {
74
63
t := t + 1;
75
64
}
76
65
}
77
66
78
-
print "Estimated parameter for BernoulliRational(1, 5): ", (t asreal) / (n asreal), " (should be around 0.2)\n";
67
+
print "Estimated parameter for Bernoulli(1, 5): ", (t asreal) / (n asreal), " (should be around 0.2)\n";
79
68
80
69
t := 0;
81
70
for i := 0 to n {
82
-
var b := r.BernoulliRational(0, 5);
71
+
var b := r.Bernoulli(Rationals.Rational(0, 5));
83
72
if b {
84
73
t := t + 1;
85
74
}
86
75
}
87
76
88
-
print "Estimated parameter for BernoulliRational(0, 5): ", (t asreal) / (n asreal), " (should be around 0.0)\n";
89
-
90
-
t := 0;
91
-
for i := 0 to n {
92
-
var b := r.BernoulliRational(5, 5);
93
-
if b {
94
-
t := t + 1;
95
-
}
96
-
}
97
-
98
-
print "Estimated parameter for BernoulliRational(5, 5): ", (t asreal) / (n asreal), " (should be around 1.0\n";
99
-
77
+
print "Estimated parameter for Bernoulli(0, 5): ", (t asreal) / (n asreal), " (should be around 0.0)\n";
100
78
101
79
t := 0;
102
80
for i := 0 to n {
103
-
var b := r.Bernoulli(0.2);
81
+
var b := r.Bernoulli(Rationals.Rational(5, 5));
104
82
if b {
105
83
t := t + 1;
106
84
}
107
85
}
108
86
109
-
print "Estimated parameter for Bernoulli(0.2): ", (t asreal) / (n asreal), " (should be around 0.2)\n";
87
+
print "Estimated parameter for Bernoulli(5, 5): ", (t asreal) / (n asreal), " (should be around 1.0\n";
110
88
111
89
t := 0;
112
90
for i := 0 to n {
113
-
var u := r.BernoulliExpNeg(2.30258509299); // about -ln(0.1)
91
+
var u := r.BernoulliExpNeg(Rationals.Rational(12381, 5377)); // about -ln(0.1)
114
92
if u {
115
93
t := t + 1;
116
94
}
@@ -121,7 +99,7 @@ module RandomExamples {
121
99
var count1 := 0;
122
100
var countneg1 := 0;
123
101
for i := 0 to n {
124
-
var u := r.DiscreteLaplace(5, 7); // DiscreteLaplace(7/5)
102
+
var u := r.DiscreteLaplace(Rationals.Rational(7, 5));
125
103
match u {
126
104
case-1 => countneg1 := countneg1 + 1;
127
105
case 0 => count0 := count0 + 1;
@@ -138,7 +116,7 @@ module RandomExamples {
138
116
count1 := 0;
139
117
countneg1 := 0;
140
118
for i := 0 to n {
141
-
var u := r.DiscreteGaussian(1.4);
119
+
var u := r.DiscreteGaussian(Rationals.Rational(7, 5));
Copy file name to clipboardExpand all lines: docs/dafny/ExamplesFoundational.dfy
+10-31Lines changed: 10 additions & 31 deletions
Original file line number
Diff line number
Diff line change
@@ -8,6 +8,7 @@
8
8
include "../../src/Dafny-VMC.dfy"
9
9
10
10
module RandomExamples {
11
+
import Rationals
11
12
import DafnyVMC
12
13
13
14
methodMain()
@@ -55,61 +56,39 @@ module RandomExamples {
55
56
}
56
57
print "Estimated probabilities for UniformInterval(7,10): ", (a asreal) / (n asreal), "; ", (b asreal) / (n asreal), "; " , (c asreal) / (n asreal), " (each should be around 0.33)\n";
57
58
58
-
a := 0;
59
-
b := 0;
60
-
for i := 0 to n {
61
-
var k := r.Geometric();
62
-
if k == 5 {
63
-
a := a + 1;
64
-
} elseif k == 10 {
65
-
b := b + 1;
66
-
}
67
-
}
68
-
print "Estimated probabilities for Geometric(0.5): " , (a asreal) / (n asreal), " (should be around 0.015625) and " , (b asreal) / (n asreal), " (should be around 0.00048828125) \n";
69
-
70
-
t := 0;
71
-
for i := 0 to n {
72
-
var b := r.BernoulliRational(1, 5);
73
-
if b {
74
-
t := t + 1;
75
-
}
76
-
}
77
-
78
-
print "Estimated parameter for BernoulliRational(1, 5): ", (t asreal) / (n asreal), " (should be around 0.2)\n";
79
-
80
59
t := 0;
81
60
for i := 0 to n {
82
-
var b := r.BernoulliRational(0, 5);
61
+
var b := r.Bernoulli(Rationals.Rational(1, 5));
83
62
if b {
84
63
t := t + 1;
85
64
}
86
65
}
87
66
88
-
print "Estimated parameter for BernoulliRational(0, 5): ", (t asreal) / (n asreal), " (should be around 0.0)\n";
67
+
print "Estimated parameter for Bernoulli(1/5): ", (t asreal) / (n asreal), " (should be around 0.2)\n";
89
68
90
69
t := 0;
91
70
for i := 0 to n {
92
-
var b := r.BernoulliRational(5, 5);
71
+
var b := r.Bernoulli(Rationals.Rational(0, 5));
93
72
if b {
94
73
t := t + 1;
95
74
}
96
75
}
97
76
98
-
print "Estimated parameter for BernoulliRational(5, 5): ", (t asreal) / (n asreal), " (should be around 1.0\n";
77
+
print "Estimated parameter for Bernoulli(0/5): ", (t asreal) / (n asreal), " (should be around 0.0)\n";
99
78
100
79
t := 0;
101
80
for i := 0 to n {
102
-
var b := r.Bernoulli(0.2);
81
+
var b := r.Bernoulli(Rationals.Rational(5, 5));
103
82
if b {
104
83
t := t + 1;
105
84
}
106
85
}
107
86
108
-
print "Estimated parameter for Bernoulli(0.2): ", (t asreal) / (n asreal), " (should be around 0.2)\n";
87
+
print "Estimated parameter for Bernoulli(5/5): ", (t asreal) / (n asreal), " (should be around 1.0\n";
109
88
110
89
t := 0;
111
90
for i := 0 to n {
112
-
var u := r.BernoulliExpNeg(2.30258509299); // about -ln(0.1)
91
+
var u := r.BernoulliExpNeg(Rationals.Rational(12381, 5377)); // about -ln(0.1)
113
92
if u {
114
93
t := t + 1;
115
94
}
@@ -120,7 +99,7 @@ module RandomExamples {
120
99
var count1 := 0;
121
100
var countneg1 := 0;
122
101
for i := 0 to n {
123
-
var u := r.DiscreteLaplace(5, 7); // DiscreteLaplace(7/5)
102
+
var u := r.DiscreteLaplace(Rationals.Rational(7, 5));
124
103
match u {
125
104
case-1 => countneg1 := countneg1 + 1;
126
105
case 0 => count0 := count0 + 1;
@@ -137,7 +116,7 @@ module RandomExamples {
137
116
count1 := 0;
138
117
countneg1 := 0;
139
118
for i := 0 to n {
140
-
var u := r.DiscreteGaussian(1.4);
119
+
var u := r.DiscreteGaussian(Rationals.Rational(7, 5));
$DAFNY audit $file| grep -v '{:termination false}\|{:extern}\|decreases *\|Dafny auditor completed\|Dafny program verifier'| sed 's/.*Warning://'| sed 's/Possible.*//'>> audit.log
16
+
$DAFNY audit $file| grep -v '{:termination false}\|{:extern}\|decreases *\|Dafny auditor completed\|Dafny program verifier\|No terms found to trigger on\|Compiled declaration has no body'| sed 's/.*Warning://'| sed 's/Possible.*//'>> audit.log
0 commit comments