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

updated proof sessions

Browse Source
This commit is contained in:
Jean-Christophe Filliatre
2017-05-16 15:48:05 +02:00
parent 3698ea2ec5
commit f868ab16f7
20 changed files with 1257 additions and 1706 deletions
Download Patch File Download Diff File Expand all files Collapse all files

9
examples/decrease1.mlw
View File

@@ -14,9 +14,12 @@ module Decrease1
predicate decrease1 (a: array int) =
forall i: int. 0 <= i < length a - 1 -> a[i+1] >= a[i] - 1
lemma decrease1_induction:
forall a: array int. decrease1 a ->
forall i j: int. 0 <= i <= j < length a -> a[j] >= a[i] + i - j
let rec lemma decrease1_induction (a: array int) (i j: int) : unit
requires { decrease1 a }
requires { 0 <= i <= j < length a }
ensures { a[j] >= a[i] + i - j }
variant { j - i }
= if i < j then decrease1_induction a (i+1) j
exception Found