vstte10_aqueue.mlw 1.5 KB
 Jean-Christophe Filliatre committed Jun 22, 2011 1 2 3 4 ``````(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html Problem 5: amortized queue `````` Jean-Christophe Filliatre committed Jul 05, 2011 5 6 `````` Author: Jean-Christophe Filliatre (CNRS) Tool: Why3 (see http://why3.lri.fr/) `````` Jean-Christophe Filliatre committed Jun 22, 2011 7 ``````*) `````` Jean-Christophe Filliatre committed Nov 10, 2010 8 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 9 10 ``````module AmortizedQueue `````` Andrei Paskevich committed Jun 15, 2018 11 12 13 `````` use int.Int use option.Option use list.ListRich `````` Jean-Christophe Filliatre committed Nov 10, 2010 14 `````` `````` Andrei Paskevich committed Oct 13, 2012 15 16 `````` type queue 'a = { front: list 'a; lenf: int; rear : list 'a; lenr: int; } `````` Guillaume Melquiond committed Mar 16, 2016 17 `````` invariant { length front = lenf >= length rear = lenr } `````` Andrei Paskevich committed Jun 26, 2017 18 `````` by { front = Nil; lenf = 0; rear = Nil; lenr = 0 } `````` Jean-Christophe Filliatre committed Jun 22, 2011 19 `````` `````` Andrei Paskevich committed Jun 29, 2011 20 `````` function sequence (q: queue 'a) : list 'a = `````` Jean-Christophe Filliatre committed Jun 22, 2011 21 22 `````` q.front ++ reverse q.rear `````` Andrei Paskevich committed Jun 26, 2017 23 24 25 `````` let empty () : queue 'a ensures { sequence result = Nil } = { front = Nil; lenf = 0; rear = Nil; lenr = 0 } `````` Jean-Christophe Filliatre committed Jun 22, 2011 26 `````` `````` Jean-Christophe Filliatre committed Apr 05, 2018 27 `````` let head (q: queue 'a) : 'a `````` Andrei Paskevich committed Oct 13, 2012 28 `````` requires { sequence q <> Nil } `````` Jean-Christophe Filliatre committed Apr 05, 2018 29 `````` ensures { hd (sequence q) = Some result } `````` Andrei Paskevich committed Jun 26, 2017 30 `````` = let Cons x _ = q.front in x `````` Jean-Christophe Filliatre committed Jun 22, 2011 31 `````` `````` Jean-Christophe Filliatre committed Apr 05, 2018 32 `````` let create (f: list 'a) (lf: int) (r: list 'a) (lr: int) : queue 'a `````` Andrei Paskevich committed Oct 13, 2012 33 `````` requires { lf = length f /\ lr = length r } `````` Jean-Christophe Filliatre committed Apr 05, 2018 34 `````` ensures { sequence result = f ++ reverse r } `````` Andrei Paskevich committed Oct 13, 2012 35 36 `````` = if lf >= lr then { front = f; lenf = lf; rear = r; lenr = lr } `````` Jean-Christophe Filliatre committed Jun 22, 2011 37 38 `````` else let f = f ++ reverse r in `````` Andrei Paskevich committed Oct 13, 2012 39 `````` { front = f; lenf = lf + lr; rear = Nil; lenr = 0 } `````` Jean-Christophe Filliatre committed Jun 22, 2011 40 `````` `````` Jean-Christophe Filliatre committed Apr 05, 2018 41 `````` let tail (q: queue 'a) : queue 'a `````` Andrei Paskevich committed Oct 13, 2012 42 `````` requires { sequence q <> Nil } `````` Jean-Christophe Filliatre committed Apr 05, 2018 43 `````` ensures { tl (sequence q) = Some (sequence result) } `````` Andrei Paskevich committed Jun 26, 2017 44 45 `````` = let Cons _ r = q.front in create r (q.lenf - 1) q.rear q.lenr `````` Jean-Christophe Filliatre committed Jun 22, 2011 46 `````` `````` Jean-Christophe Filliatre committed Apr 05, 2018 47 `````` let enqueue (x: 'a) (q: queue 'a) : queue 'a `````` Andrei Paskevich committed Oct 13, 2012 48 49 `````` ensures { sequence result = sequence q ++ Cons x Nil } = create q.front q.lenf (Cons x q.rear) (q.lenr + 1) `````` Jean-Christophe Filliatre committed Nov 10, 2010 50 `````` `````` Jean-Christophe Filliatre committed Dec 29, 2010 51 ``end``