kmc7468/cs220
1
0 Fork 0
mirror of https://github.com/kmc7468/cs220.git synced 2026-11-04 00:00:33 +09:00
Code Issues Packages Projects Releases Wiki Activity

Strengthen the post-condition

Browse Source
This commit is contained in:
Jeehoon Kang committed 2022-09-28 23:15:39 +09:00
1 parent 85fd0b333b
commit 3a463b55b1
1 file changed
+1 -1
Download Patch File Download Diff File Expand all files Collapse all files
assets/why3/binary_search.mlw
+1 -1
View File
@@ -15,7 +15,7 @@ module BinarySearch
requires { forall i1 i2 : int. 0 <= i1 < i2 < length a -> a[i1] <= a[i2] } requires { forall i1 i2 : int. 0 <= i1 < i2 < length a -> a[i1] <= a[i2] }
ensures { 0 <= result <= length a } ensures { 0 <= result <= length a }
ensures { forall i: int. 0 <= i < result -> a[i] < v } ensures { forall i: int. 0 <= i < result -> a[i] < v }
ensures { result < length a -> a[result] >= v } ensures { forall i: int. result <= i < length a -> v <= a[i] }
= =
(* IMPORTANT: DON'T MODIFY THE ABOVE LINES *) (* IMPORTANT: DON'T MODIFY THE ABOVE LINES *)
0 (* TODO *) 0 (* TODO *)