ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity

gallery: more proofs of termination

Browse Source
This commit is contained in:
Jean-Christophe Filliatre
2014-01-22 18:13:26 +01:00
parent 7ee0bf01cd
commit 397e8c4d7d
2 changed files with 55 additions and 14 deletions
Download Patch File Download Diff File Expand all files Collapse all files

7
examples/decrease1.mlw
View File

@@ -43,9 +43,10 @@ module Decrease1
let rec search_rec (a: array int) (i : int)
requires { decrease1 a /\ 0 <= i }
ensures {
(result = -1 /\ forall j: int. i <= j < length a -> a[j] <> 0)
\/ (i <= result < length a /\ a[result] = 0 /\
forall j: int. i <= j < result -> a[j] <> 0) }
(result = -1 /\ forall j: int. i <= j < length a -> a[j] <> 0)
\/ (i <= result < length a /\ a[result] = 0 /\
forall j: int. i <= j < result -> a[j] <> 0) }
variant { length a - i }
= if i < length a then
if a[i] = 0 then i
else if a[i] > 0 then search_rec a (i + a[i])