python.mlw 1.06 KB
Newer Older
1 2 3 4 5

module Python

  use import int.Int
  use import ref.Ref
6
  use array.Array as A
7

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

  function ([]) (l: list 'a) (i: int) : 'a =
12
    A.get l i
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
13 14

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

  let len (l: list 'a) : int
    ensures { result = len(l) }
  = A.length l
20 21

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

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

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

37 38 39 40 41
  (* TODO: specify division and modulus according to
     https://docs.python.org/3/reference/expressions.html *)
  function div int int : int
  function mod int int : int

42 43 44 45
  val randint (l u: int) : int
    requires { l <= u }
    ensures  { l <= result <= u }

46
end