Commit 490e6428 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files


parent 8af3f3c1
......@@ -44,13 +44,13 @@ module FactImperative
(* Checking a large routine Alan Mathison Turing, 1949
(* 'Checking a large routine' Alan Mathison Turing, 1949
One of the earliest proof of program.
The routine computes n! using only additions, using two nested loops.
The routine computes n! using only additions, with two nested loops.
module CheckingALargRoutine
module CheckingALargeRoutine
use import Fact
use import int.Int
......@@ -18,7 +18,7 @@
<theory name="WP CheckingALargRoutine" verified="true" expanded="true">
<theory name="WP CheckingALargeRoutine" verified="true" expanded="true">
<goal name="WP_parameter routine" expl="correctness of parameter routine" sum="8ff7c5f56f6c843793a6ab7586cce14c" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter routine.1" expl="loop invariant init" sum="9a5b92f18bf024980c5dd8bdcfdfba50" proved="true" expanded="true">
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment