library: {Stack,Queue}.length now return a Peano.t

this way, the extraction maps them to OCaml's {Stack,Queue}.length
without using ZArith anymore
parent 2627b74e
...@@ -144,7 +144,7 @@ module stack.Stack ...@@ -144,7 +144,7 @@ module stack.Stack
syntax val clear "Stack.clear" syntax val clear "Stack.clear"
syntax val copy "Stack.copy" syntax val copy "Stack.copy"
syntax val is_empty "Stack.is_empty" syntax val is_empty "Stack.is_empty"
syntax val length "Z.of_int (Stack.length %1)" syntax val length "Stack.length %1"
end end
module queue.Queue module queue.Queue
...@@ -159,7 +159,7 @@ module queue.Queue ...@@ -159,7 +159,7 @@ module queue.Queue
syntax val clear "Queue.clear" syntax val clear "Queue.clear"
syntax val copy "Queue.copy" syntax val copy "Queue.copy"
syntax val is_empty "Queue.is_empty" syntax val is_empty "Queue.is_empty"
syntax val length "(Z.of_int (Queue.length %1))" syntax val length "Queue.length %1"
syntax val transfer "Queue.transfer" syntax val transfer "Queue.transfer"
end end
......
...@@ -24,16 +24,16 @@ module MergesortQueue ...@@ -24,16 +24,16 @@ module MergesortQueue
requires { q.elts = Nil /\ sorted q1.elts /\ sorted q2.elts } requires { q.elts = Nil /\ sorted q1.elts /\ sorted q2.elts }
ensures { sorted q.elts } ensures { sorted q.elts }
ensures { permut q.elts (old q1.elts ++ old q2.elts) } ensures { permut q.elts (old q1.elts ++ old q2.elts) }
= while length q1 > 0 || length q2 > 0 do = while not (is_empty q1 && is_empty q2) do
invariant { sorted q1.elts /\ sorted q2.elts /\ sorted q.elts } invariant { sorted q1.elts /\ sorted q2.elts /\ sorted q.elts }
invariant { forall x y: elt. mem x q.elts -> mem y q1.elts -> le x y } invariant { forall x y: elt. mem x q.elts -> mem y q1.elts -> le x y }
invariant { forall x y: elt. mem x q.elts -> mem y q2.elts -> le x y } invariant { forall x y: elt. mem x q.elts -> mem y q2.elts -> le x y }
invariant { permut (q.elts ++ q1.elts ++ q2.elts) invariant { permut (q.elts ++ q1.elts ++ q2.elts)
(old (q1.elts ++ q2.elts)) } (old (q1.elts ++ q2.elts)) }
variant { length q1 + length q2 } variant { length q1 + length q2 }
if length q1 = 0 then if is_empty q1 then
push (safe_pop q2) q push (safe_pop q2) q
else if length q2 = 0 then else if is_empty q2 then
push (safe_pop q1) q push (safe_pop q1) q
else else
let x1 = safe_peek q1 in let x1 = safe_peek q1 in
...@@ -47,7 +47,7 @@ module MergesortQueue ...@@ -47,7 +47,7 @@ module MergesortQueue
let rec mergesort (q: t elt) : unit let rec mergesort (q: t elt) : unit
ensures { sorted q.elts /\ permut q.elts (old q.elts) } ensures { sorted q.elts /\ permut q.elts (old q.elts) }
variant { length q } variant { length q }
= if length q > 1 then begin = if Peano.gt (length q) Peano.one then begin
let q1 = create () : t elt in let q1 = create () : t elt in
let q2 = create () : t elt in let q2 = create () : t elt in
while not (is_empty q) do while not (is_empty q) do
......
This diff is collapsed.
...@@ -44,10 +44,10 @@ ...@@ -44,10 +44,10 @@
</theory> </theory>
<theory name="GilbreathCardTrick" proved="true"> <theory name="GilbreathCardTrick" proved="true">
<goal name="VC shuffle" expl="VC for shuffle" proved="true"> <goal name="VC shuffle" expl="VC for shuffle" proved="true">
<proof prover="2"><result status="valid" time="1.16" steps="3279"/></proof> <proof prover="2"><result status="valid" time="0.84" steps="3281"/></proof>
</goal> </goal>
<goal name="VC card_trick" expl="VC for card_trick" proved="true"> <goal name="VC card_trick" expl="VC for card_trick" proved="true">
<proof prover="2"><result status="valid" time="0.16" steps="614"/></proof> <proof prover="2"><result status="valid" time="0.16" steps="616"/></proof>
</goal> </goal>
</theory> </theory>
</file> </file>
......
...@@ -98,26 +98,26 @@ ...@@ -98,26 +98,26 @@
<proof prover="5"><result status="valid" time="0.00" steps="6"/></proof> <proof prover="5"><result status="valid" time="0.00" steps="6"/></proof>
</goal> </goal>
<goal name="VC process_queue" expl="VC for process_queue" proved="true"> <goal name="VC process_queue" expl="VC for process_queue" proved="true">
<proof prover="5"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="6"/></proof>
</goal> </goal>
<goal name="VC rt_empty" expl="VC for rt_empty" proved="true"> <goal name="VC rt_empty" expl="VC for rt_empty" proved="true">
<proof prover="5"><result status="valid" time="0.01" steps="7"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="9"/></proof>
</goal> </goal>
<goal name="VC rt_get" expl="VC for rt_get" proved="true"> <goal name="VC rt_get" expl="VC for rt_get" proved="true">
<proof prover="5"><result status="valid" time="0.01" steps="8"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="10"/></proof>
</goal> </goal>
<goal name="VC rt_add" expl="VC for rt_add" proved="true"> <goal name="VC rt_add" expl="VC for rt_add" proved="true">
<transf name="split_goal_right" proved="true" > <transf name="split_goal_right" proved="true" >
<goal name="VC rt_add.0" expl="precondition" proved="true"> <goal name="VC rt_add.0" expl="precondition" proved="true">
<transf name="split_goal_right" proved="true" > <transf name="split_goal_right" proved="true" >
<goal name="VC rt_add.0.0" expl="VC for rt_add" proved="true"> <goal name="VC rt_add.0.0" expl="VC for rt_add" proved="true">
<proof prover="5"><result status="valid" time="0.00" steps="4"/></proof> <proof prover="5"><result status="valid" time="0.00" steps="6"/></proof>
</goal> </goal>
<goal name="VC rt_add.0.1" expl="VC for rt_add" proved="true"> <goal name="VC rt_add.0.1" expl="VC for rt_add" proved="true">
<proof prover="5"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="6"/></proof>
</goal> </goal>
<goal name="VC rt_add.0.2" expl="VC for rt_add" proved="true"> <goal name="VC rt_add.0.2" expl="VC for rt_add" proved="true">
<proof prover="5"><result status="valid" time="0.01" steps="17"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="19"/></proof>
</goal> </goal>
<goal name="VC rt_add.0.3" expl="VC for rt_add" proved="true"> <goal name="VC rt_add.0.3" expl="VC for rt_add" proved="true">
<proof prover="0"><result status="valid" time="0.82"/></proof> <proof prover="0"><result status="valid" time="0.82"/></proof>
...@@ -125,13 +125,13 @@ ...@@ -125,13 +125,13 @@
</transf> </transf>
</goal> </goal>
<goal name="VC rt_add.1" expl="postcondition" proved="true"> <goal name="VC rt_add.1" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.01" steps="8"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="10"/></proof>
</goal> </goal>
<goal name="VC rt_add.2" expl="precondition" proved="true"> <goal name="VC rt_add.2" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="57"/></proof> <proof prover="5"><result status="valid" time="0.03" steps="59"/></proof>
</goal> </goal>
<goal name="VC rt_add.3" expl="postcondition" proved="true"> <goal name="VC rt_add.3" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.01" steps="7"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="9"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
......
This source diff could not be displayed because it is too large. You can view the blob instead.
...@@ -3,6 +3,7 @@ ...@@ -3,6 +3,7 @@
module Queue module Queue
use mach.peano.Peano
use list.List use list.List
use list.Append use list.Append
use list.Length as L use list.Length as L
...@@ -45,7 +46,7 @@ module Queue ...@@ -45,7 +46,7 @@ module Queue
function length (q: t 'a) : int = L.length q.elts function length (q: t 'a) : int = L.length q.elts
val length (q: t 'a) : int val length (q: t 'a) : Peano.t
ensures { result = L.length q.elts } ensures { result = L.length q.elts }
val transfer (q1 q2: t 'a) : unit val transfer (q1 q2: t 'a) : unit
......
...@@ -5,6 +5,7 @@ ...@@ -5,6 +5,7 @@
module Stack module Stack
use mach.peano.Peano
use list.List use list.List
use list.Length as L use list.Length as L
...@@ -46,7 +47,7 @@ module Stack ...@@ -46,7 +47,7 @@ module Stack
function length (s: t 'a) : int = L.length s.elts function length (s: t 'a) : int = L.length s.elts
val length (s: t 'a) : int val length (s: t 'a) : Peano.t
ensures { result = L.length s.elts } ensures { result = L.length s.elts }
end end
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