Commit 50513e70 authored by Andrei Paskevich's avatar Andrei Paskevich

python: add the element preservation property for insertion sort

In a different file, so that we can show the simpler ordering property
first.

Also, I cheat, and add an appropriate lemma to modules/python.mlw.
Maybe this is a good lemma to have in map.Occ, too.
parent 820c7bbd
module MapOcc
use import int.Int
use import map.Map
use import map.Occ
lemma occ_exchange :
forall m: map int 'a, l u i j: int, x y z: 'a.
l <= i < u ->
l <= j < u ->
Occ.occ z m[i <- x][j <- y] l u =
Occ.occ z m[i <- y][j <- x] l u
end
module Python
......@@ -11,6 +23,9 @@ module Python
function ([]) (l: list 'a) (i: int) : 'a =
Array.get l i
function ([<-]) (l: list 'a) (i: int) (v: 'a) : list 'a =
Array.set l i v
function len (l: list 'a) : int =
Array.length l
......@@ -34,6 +49,13 @@ module Python
ensures { Array.length result = u - l }
ensures { forall i. l <= i < u -> result[i] = i }
(* ad-hoc facts about exchange *)
use MapOcc
function occurrence (v: 'a) (l: list 'a) : int =
MapOcc.Occ.occ v l.Array.elts 0 l.Array.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 *)
......
from random import randint
n = 42
a = [0] * n
### On remplit le tableau "a"
for i in range(0, len(a)):
a[i] = randint(0, 100)
print(a)
### On prend une photo de "a"
photo = [0] * n
k = 0
while k < len(a):
#@ invariant 0 <= k <= len(a)
#@ invariant forall i. 0 <= i < k -> photo[i] == a[i]
#@ variant len(a) - k
photo[k] = a[k]
k = k + 1
#@ assert forall i. 0 <= i < len(a) -> photo[i] == a[i]
### Et maintenant on le trie
m = 1
while m < len(a):
#@ invariant 1 <= m <= len(a)
#@ invariant forall i,j. 0 <= i <= j < m -> a[i] <= a[j]
#@ invariant forall v. occurrence(v, a) == occurrence(v, photo)
#@ variant len(a) - m
x = a[m]
k = m
while k > 0 and a[k-1] > x:
#@ invariant 0 <= k <= m
#@ invariant forall i,j. 0 <= i <= j < k -> a[i] <= a[j]
#@ invariant forall i,j. 0 <= i < k < j <= m -> a[i] <= a[j]
#@ invariant forall i,j. k < i <= j <= m -> a[i] <= a[j]
#@ invariant forall j. k < j <= m -> x < a[j]
#@ invariant forall v. occurrence(v, a[k <- x]) == occurrence(v, photo)
#@ variant k
a[k] = a[k-1]
k = k - 1
a[k] = x
m = m + 1
#@ assert forall i,j. 0 <= i <= j < len(a) -> a[i] <= a[j]
#@ assert forall v. occurrence(v, a) == occurrence(v, photo)
print(a)
......@@ -4,11 +4,15 @@ from random import randint
n = 42
a = [0] * n
### On remplit le tableau "a"
for i in range(0, len(a)):
a[i] = randint(0, 100)
print(a)
### Et maintenant on le trie
m = 1
while m < len(a):
#@ invariant 1 <= m <= len(a)
......@@ -21,7 +25,7 @@ while m < len(a):
#@ invariant forall i,j. 0 <= i <= j < k -> a[i] <= a[j]
#@ invariant forall i,j. 0 <= i < k < j <= m -> a[i] <= a[j]
#@ invariant forall i,j. k < i <= j <= m -> a[i] <= a[j]
#@ invariant forall j. k < j <= m -> x < a[j]
#@ invariant forall j. k < j <= m -> x < a[j]
#@ variant k
a[k] = a[k-1]
k = k - 1
......
......@@ -105,7 +105,8 @@ rule next_tokens = parse
| ':' { [COLON] }
(* logic symbols *)
| "->" { [ARROW] }
| "->" { [LRARROW] }
| "<-" { [LARROW] }
| "<->" { [LRARROW] }
| "." { [DOT] }
| integer as s
{ [INTEGER s] }
......
......@@ -39,6 +39,7 @@
let mixfix s = "mixfix " ^ s
let get_op s e = Qident (mk_id (mixfix "[]") s e)
let set_op s e = Qident (mk_id (mixfix "[<-]") s e)
let empty_spec = {
sp_pre = []; sp_post = []; sp_xpost = [];
......@@ -70,7 +71,7 @@
%token PLUS MINUS TIMES DIV MOD
(* annotations *)
%token INVARIANT VARIANT ASSUME ASSERT CHECK REQUIRES ENSURES LABEL
%token ARROW LRARROW FORALL EXISTS DOT THEN LET
%token ARROW LARROW LRARROW FORALL EXISTS DOT THEN LET
(* precedences *)
......@@ -299,6 +300,8 @@ term_sub_:
| LEFTPAR term RIGHTPAR { $2.term_desc }
| term_arg LEFTSQ term RIGHTSQ
{ Tidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
| term_arg LEFTSQ term LARROW term RIGHTSQ
{ Tidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) }
%inline bin_op:
| ARROW { Timplies }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment