stdlib/python.mlw

   1 module Python
   2
   3   use int.Int
   4   use ref.Ref
   5   use seq.Seq
   6   use int.EuclideanDivision as E
   7
   8   type list 'a = private {
   9     mutable elts: seq 'a;
  10     mutable len: int;
  11   } invariant { len = length elts }
  12
  13   meta coercion function elts
  14
  15   function ([]) (l: list 'a) (i: int) : 'a
  16   = [@inline:trivial]
  17     if i >= 0 then Seq.(l[i]) else Seq.(l[l.len + i])
  18
  19   val ghost function create (s: seq 'a) : list 'a
  20     ensures { result = s }
  21     ensures { len result = length s }
  22
  23   function ([<-]) (l: list 'a) (i: int) (v: 'a) : list 'a
  24   = [@inline:trivial]
  25     create (if i >= 0 then Seq.(l.elts[i <- v]) else Seq.(l.elts[l.len + i <- v]))
  26
  27   let ([]) (l: list 'a) (i: int) : 'a
  28     requires { [@expl:index in array bounds] -len l <= i < len l }
  29     ensures  { result = l[i] }
  30   = if i >= 0 then Seq.(l.elts[i]) else Seq.(l.elts[len l + i])
  31
  32   val ([]<-) (l: list 'a) (i: int) (v: 'a) : unit
  33     requires { [@expl:index in array bounds] -len l <= i < len l }
  34     writes   { l.elts }
  35     ensures  { l.elts = (old l)[i <- v].elts }
  36
  37   val empty () : list 'a
  38     ensures { result = Seq.empty }
  39
  40   val make (n: int) (v: 'a) : list 'a
  41     requires { n >= 0 }
  42     ensures  { len result = n }
  43     ensures  { forall i. -n <= i < n -> result[i] = v }
  44
  45
  46   (* ad-hoc facts about exchange *)
  47
  48   use seq.Occ
  49
  50   function occurrence (v: 'a) (l: list 'a) (lo hi: int): int =
  51     Occ.occ v l lo hi
  52
  53   use int.Abs
  54
  55   (* Python's division and modulus according are neither Euclidean division,
  56    nor computer division, but something else defined in
  57    https://docs.python.org/3/reference/expressions.html *)
  58
  59   function (//) (x y: int) : int =
  60     let q = E.div x y in
  61     if y >= 0 then q else if E.mod x y > 0 then q-1 else q
  62   function (%) (x y: int) : int =
  63     let r = E.mod x y in
  64     if y >= 0 then r else if r > 0 then r+y else r
  65
  66   lemma div_mod:
  67     forall x y:int. y <> 0 -> x = y * (x // y) + (x % y)
  68   lemma mod_bounds:
  69     forall x y:int. y <> 0 -> 0 <= abs (x % y) < abs y
  70   lemma mod_sign:
  71     forall x y:int. y <> 0 -> if y < 0 then x % y <= 0 else x % y >= 0
  72
  73   val (//) (x y: int) : int
  74     requires { [@expl:check division by zero] y <> 0 }
  75     ensures  { result = x // y }
  76
  77   val (%) (x y: int) : int
  78     requires { [@expl:check division by zero] y <> 0 }
  79     ensures  { result = x % y }
  80
  81   (* random.randint *)
  82   val randint (l u: int) : int
  83     requires { [@expl:valid range] l <= u }
  84     ensures  { l <= result <= u }
  85
  86   use int.Power
  87
  88   function pow (x y: int) : int = power x y
  89
  90   val input () : int
  91
  92   val int (n: int) : int
  93     ensures { result = n }
  94
  95   (* ajouts réalisés *)
  96
  97   val range (lo hi: int) : list int
  98     requires { [@expl:valid range] lo <= hi }
  99     ensures  { len result = hi - lo }
 100     ensures  { forall i. 0 <= i < hi - lo -> result[i] = i + lo }
 101
 102   let range3 (le ri step: int) : list int
 103     requires { [@expl:valid range] (le <= ri /\ step > 0) \/ (ri <= le /\ step < 0) }
 104     ensures  { len result = E.div (ri - le) step + if E.mod (ri - le) step <> 0 then 1 else 0 }
 105     ensures  { forall i. 0 <= i < len result -> result[i] = le + i * step }
 106   = let n = E.div (ri - le) step + if E.mod (ri - le) step <> 0 then 1 else 0 in
 107     let a = make n 0 in
 108     for i=0 to n-1 do
 109       invariant { forall j. 0 <= j < i -> a[j] = le + j * step }
 110       a[i] <- le + i * step;
 111     done;
 112     assert { step > 0 -> le +  n    * step >= ri
 113           /\ step > 0 -> le + (n-1) * step <  ri
 114           /\ step < 0 -> le +  n    * step <= ri
 115           /\ step < 0 -> le + (n-1) * step >  ri };
 116     return a
 117
 118   val pop (l: list 'a) : 'a
 119     requires { len l > 0 }
 120     writes   { l }
 121     ensures  { len l = len (old l) - 1 }
 122     ensures  { result = (old l)[len l] }
 123     ensures  { forall i. 0 <= i < len l -> l[i] = (old l)[i] }
 124
 125   val append (l: list 'a) (v: 'a) : unit
 126     writes   { l }
 127     ensures  { len l = len (old l) + 1 }
 128     ensures  { l[len (old l)] = v }
 129     ensures  { forall i. 0 <= i < len (old l) -> l[i] = (old l)[i] }
 130
 131   val function add_list (a1: list 'a) (a2: list 'a) : list 'a
 132     ensures { len result = len a1 + len a2 }
 133     ensures { forall i. 0 <= i < len a1 -> result[i] = a1[i] }
 134     ensures { forall i. len a1 <= i < len result -> result[i] = a2[i-len a1] }
 135
 136   function transform_idx (l: list 'a) (i: int): int
 137   = [@inline:trivial]
 138     if i < 0 then len l + i else i
 139
 140   val function slice (l: list 'a) (lo hi: int) : list 'a
 141     requires { transform_idx l lo >= 0 }
 142     requires { transform_idx l hi <= len l }
 143     requires { transform_idx l lo <= transform_idx l hi }
 144     ensures  { len result = transform_idx l hi - transform_idx l lo }
 145     ensures  { forall i. 0 <= i < len result -> result[i] = l[transform_idx l lo + i] }
 146
 147   val clear (l : list 'a) : unit
 148     writes  { l }
 149     ensures { len l = 0 }
 150
 151   val copy (l: list 'a): list 'a
 152     ensures { len result = len l }
 153     ensures { result.elts = l.elts }
 154
 155   use seq.Permut
 156
 157   predicate is_permutation (l1 l2: list 'a)
 158   = ([@expl:equality of length] length l1 = length l2)
 159       /\ ([@expl:equality of elements] permut l1 l2 0 (length l2))
 160
 161   val sort (l : list int) : unit
 162     writes  { l.elts }
 163     ensures { is_permutation l (old l) }
 164     ensures { forall i, j. 0 <= i <= j < len(l) -> l[i] <= l[j] }
 165
 166   val reverse (l: list 'a) : unit
 167     writes  { l.elts }
 168     ensures { len l = len (old l) }
 169     ensures { forall i. 0 <= i < len l -> l[i] = (old l)[-(i+1)] }
 170     ensures { forall i. 0 <= i < len l -> (old l)[i] = l[-(i+1)] }
 171     ensures { is_permutation l (old l) }
 172
 173 end