module Python use int.Int use ref.Ref use array.Array as A (* Python's lists are actually resizable arrays, but we simplify here *) type list 'a = A.array 'a function ([]) (l: list 'a) (i: int) : 'a = A.([]) l i function ([<-]) (l: list 'a) (i: int) (v: 'a) : list 'a = A.([<-]) l i v let function len (l: list 'a) : int = A.length l let ([]) (l: list 'a) (i: int) : 'a requires { 0 <= i < A.length l } ensures { result = l[i] } = A.([]) l i let ([]<-) (l: list 'a) (i: int) (v: 'a) : unit requires { 0 <= i < A.length l } writes { l } ensures { l = A.([<-]) (old l) i v } = A.([]<-) l i v val range (l u: int) : list int requires { l <= u } ensures { A.length result = u - l } ensures { forall i. l <= i < u -> result[i] = i } (* ad-hoc facts about exchange *) use map.Occ function occurrence (v: 'a) (l: list 'a) : int = Occ.occ v l.A.elts 0 l.A.length (* Python's division and modulus according are neither Euclidean division, nor computer division, but something else defined in https://docs.python.org/3/reference/expressions.html *) use int.Abs use int.EuclideanDivision as E function div (x y: int) : int = let q = E.div x y in if y >= 0 then q else if E.mod x y > 0 then q-1 else q function mod (x y: int) : int = let r = E.mod x y in if y >= 0 then r else if r > 0 then r+y else r lemma div_mod: forall x y:int. y <> 0 -> x = y * div x y + mod x y lemma mod_bounds: forall x y:int. y <> 0 -> 0 <= abs (mod x y) < abs y lemma mod_sign: forall x y:int. y <> 0 -> if y < 0 then mod x y <= 0 else mod x y >= 0 val (//) (x y: int) : int requires { y <> 0 } ensures { result = div x y } val (%) (x y: int) : int requires { y <> 0 } ensures { result = mod x y } (* random.randint *) val randint (l u: int) : int requires { l <= u } ensures { l <= result <= u } val input () : int val int (n: int) : int ensures { result = n } exception Break exception Return int end