Something went wrong on our end
-
Andrei Paskevich authoredAndrei Paskevich authored
python.mlw 2.03 KiB
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