python.mlw 723 Bytes
Newer Older
1 2 3 4 5 6 7

module Python

  use import int.Int
  use import ref.Ref
  use seq.Seq as S

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
8
  (* Python's lists are resizable arrays *)
9 10 11
  type list 'a = ref (S.seq 'a)

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

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

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

  let ([]<-) (l: list 'a) (i: int) (v: 'a) : unit
    requires { 0 <= i < S.length !l }
    writes   { l }
    ensures  { !l = S.set (old !l) i v }
  = l := S.set !l i v
27 28 29

  val range (l u: int) : list int
    requires { l <= u }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
30
    ensures  { S.length !result = u - l }
31 32 33
    ensures  { forall i. l <= i < u -> result[i] = i }

end