kmc7468/cs220
1
0
Fork 0
mirror of https://github.com/kmc7468/cs220.git synced 2025-12-15 06:28:46 +00:00
Code Issues Packages Projects Releases Wiki Activity

Add a warning on binary search

Browse Source
This commit is contained in:
Jeehoon Kang
2022-09-12 13:35:14 +09:00
parent 04cfaf7b77
commit 5759815506
1 changed files with 2 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
assets/why3/binary_search.mlw
View File

@@ -17,7 +17,6 @@ module BinarySearch
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 { result < length a -> a[result] >= v }
= =
let l = ref (-1) in (* IMPORTANT: DON'T MODIFY THE ABOVE LINES *)
let u = ref (length a) in 0 (* TODO *)
!u - !l (* TODO *)
end end