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

Fix binary search type

Browse Source
This commit is contained in:
Jeehoon Kang
2022-09-28 21:17:01 +09:00
parent cd4c612fb1
commit 5e2a772443
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
assets/why3/binary_search.mlw
View File

@@ -11,7 +11,7 @@ module BinarySearch
use import ref.Ref use import ref.Ref
use import array.Array use import array.Array
let binary_search (a : array int) (v : int) let binary_search (a : array int) (v : int) : int
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 }