python.mlw 2.03 KB
Newer Older
1 2
module Python

3 4
  use int.Int
  use ref.Ref
5
  use array.Array as A
6

7
  (* Python's lists are actually resizable arrays, but we simplify here *)
8
  type list 'a = A.array 'a
9 10

  function ([]) (l: list 'a) (i: int) : 'a =
11
    A.([]) l i
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
12

13
  function ([<-]) (l: list 'a) (i: int) (v: 'a) : list 'a =
14
    A.([<-]) l i v
15

16
  let function len (l: list 'a) : int
17
  = A.length l
18 19

  let ([]) (l: list 'a) (i: int) : 'a
20
    requires { 0 <= i < A.length l }
21
    ensures  { result = l[i] }
22
  = A.([]) l i
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
23 24

  let ([]<-) (l: list 'a) (i: int) (v: 'a) : unit
25
    requires { 0 <= i < A.length l }
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
26
    writes   { l }
27 28
    ensures  { l = A.([<-]) (old l) i v }
  = A.([]<-) l i v
29 30 31

  val range (l u: int) : list int
    requires { l <= u }
32
    ensures  { A.length result = u - l }
33 34
    ensures  { forall i. l <= i < u -> result[i] = i }

35 36
  (* ad-hoc facts about exchange *)

37
  use map.Occ
38 39

  function occurrence (v: 'a) (l: list 'a) : int =
40
    Occ.occ v l.A.elts 0 l.A.length
41

42 43
  (* Python's division and modulus according are neither Euclidean division,
     nor computer division, but something else defined in
44 45
     https://docs.python.org/3/reference/expressions.html *)

46
  use int.Abs
47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62
  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

63
  val (//) (x y: int) : int
64 65 66
    requires { y <> 0 }
    ensures  { result = div x y }

67
  val (%) (x y: int) : int
68 69 70 71
    requires { y <> 0 }
    ensures  { result = mod x y }

  (* random.randint *)
72 73 74 75
  val randint (l u: int) : int
    requires { l <= u }
    ensures  { l <= result <= u }

76 77
  val input () : int

78 79 80
  val int (n: int) : int
    ensures { result = n }

81 82
  exception Break

83 84
  exception Return int

85
end