From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Mon, 6 Jun 2016 23:14:18 -0600
Subject: Merging complete.  Everything looks good *crosses fingers*

---
 Test/textbook/TuringFactorial.bpl | 70 +++++++++++++++++++--------------------
 1 file changed, 35 insertions(+), 35 deletions(-)

(limited to 'Test/textbook/TuringFactorial.bpl')

diff --git a/Test/textbook/TuringFactorial.bpl b/Test/textbook/TuringFactorial.bpl
index dffc36ab..de00e3c0 100644
--- a/Test/textbook/TuringFactorial.bpl
+++ b/Test/textbook/TuringFactorial.bpl
@@ -1,35 +1,35 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// A Boogie version of Turing's additive factorial program, from "Checking a large routine"
-// published in the "Report of a Conference of High Speed Automatic Calculating Machines",
-// pp. 67-69, 1949.
-
-procedure ComputeFactorial(n: int) returns (u: int)
-  requires 1 <= n;
-  ensures u == Factorial(n);
-{
-  var r, v, s: int;
-  r, u := 1, 1;
-TOP:  // B
-  assert r <= n;
-  assert u == Factorial(r);
-  v := u;
-  if (n <= r) { return; }
-  s := 1;
-INNER:  // E
-  assert s <= r;
-  assert v == Factorial(r) && u == s * Factorial(r);
-  u := u + v;
-  s := s + 1;
-  assert s - 1 <= r;
-  if (s <= r) { goto INNER; }
-  r := r + 1;
-  goto TOP;
-}
-
-function Factorial(int): int;
-axiom Factorial(0) == 1;
-axiom (forall n: int :: {Factorial(n)}  1 <= n ==> Factorial(n) == n * Factorial_Aux(n-1));
-
-function Factorial_Aux(int): int;
-axiom (forall n: int :: {Factorial(n)} Factorial(n) == Factorial_Aux(n));
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// A Boogie version of Turing's additive factorial program, from "Checking a large routine"
+// published in the "Report of a Conference of High Speed Automatic Calculating Machines",
+// pp. 67-69, 1949.
+
+procedure ComputeFactorial(n: int) returns (u: int)
+  requires 1 <= n;
+  ensures u == Factorial(n);
+{
+  var r, v, s: int;
+  r, u := 1, 1;
+TOP:  // B
+  assert r <= n;
+  assert u == Factorial(r);
+  v := u;
+  if (n <= r) { return; }
+  s := 1;
+INNER:  // E
+  assert s <= r;
+  assert v == Factorial(r) && u == s * Factorial(r);
+  u := u + v;
+  s := s + 1;
+  assert s - 1 <= r;
+  if (s <= r) { goto INNER; }
+  r := r + 1;
+  goto TOP;
+}
+
+function Factorial(int): int;
+axiom Factorial(0) == 1;
+axiom (forall n: int :: {Factorial(n)}  1 <= n ==> Factorial(n) == n * Factorial_Aux(n-1));
+
+function Factorial_Aux(int): int;
+axiom (forall n: int :: {Factorial(n)} Factorial(n) == Factorial_Aux(n));
-- 
cgit v1.2.3