diff options
Diffstat (limited to 'Test/dafny3/Dijkstra.dfy')
| -rw-r--r-- | Test/dafny3/Dijkstra.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny3/Dijkstra.dfy b/Test/dafny3/Dijkstra.dfy index 1fbd9b7c..56719180 100644 --- a/Test/dafny3/Dijkstra.dfy +++ b/Test/dafny3/Dijkstra.dfy @@ -3,7 +3,7 @@ // Example taken from:
// Edsger W. Dijkstra: Heuristics for a Calculational Proof. Inf. Process. Lett. (IPL) 53(3):141-143 (1995)
-// Transcribed into Dafny by Valentin Wüstholz and Nadia Polikarpova.
+// Transcribed into Dafny by Valentin Wüstholz and Nadia Polikarpova.
// f is an arbitrary function on the natural numbers
function f(n: nat) : nat
@@ -56,7 +56,7 @@ lemma lemma_ping(j: nat, n: nat) }
}
-// The other directorion: f(n) <= n
+// The other direction: f(n) <= n
lemma lemma_pong(n: nat)
requires P()
ensures f(n) <= n
|