From 3ad94e1e638f727a7b862183414effc61dc1b781 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Mon, 20 Jul 2015 15:52:20 -0700 Subject: Fix encoding in Dijkstra.py --- Test/dafny3/Dijkstra.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Test/dafny3/Dijkstra.dfy') diff --git a/Test/dafny3/Dijkstra.dfy b/Test/dafny3/Dijkstra.dfy index 1fbd9b7c..42aa3b9e 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 -- cgit v1.2.3 From d0fb19ff74b0397749362beedf39ffb8d1c623a9 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 28 Aug 2015 13:42:59 -0700 Subject: Fixed spelling mistake in test file --- Test/dafny3/Dijkstra.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Test/dafny3/Dijkstra.dfy') diff --git a/Test/dafny3/Dijkstra.dfy b/Test/dafny3/Dijkstra.dfy index 42aa3b9e..56719180 100644 --- a/Test/dafny3/Dijkstra.dfy +++ b/Test/dafny3/Dijkstra.dfy @@ -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 -- cgit v1.2.3