--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/document/loop_invariant.ads	Thu Sep 22 16:50:23 2011 +0200
@@ -0,0 +1,14 @@
+package Loop_Invariant
+is
+
+   type Word32 is mod 2 ** 32;
+
+   procedure Proc1 (A : in Natural; B : in Word32; C : out Word32);
+   --# derives C from A, B;
+   --# post Word32 (A) * B = C;
+
+   procedure Proc2 (A : in Natural; B : in Word32; C : out Word32);
+   --# derives C from A, B;
+   --# post Word32 (A) * B = C;
+
+end Loop_Invariant;