binary sort: simplified code (and proof) using self_blit

parent 98cf448b
......@@ -58,12 +58,7 @@ module BinarySort
(* !left is the place where to insert value v
so we move a[!left..k) one position to the right *)
'L:
for l = k downto !left + 1 do
invariant { forall i. l < i <= k -> a[i] = (at a 'L)[i - 1] }
invariant { forall i. 0 <= i <= l -> a[i] = (at a 'L)[i] }
invariant { forall i. k < i < length a -> a[i] = (at a 'L)[i] }
a[l] <- a[l - 1]
done;
self_blit a !left (!left + 1) (k - !left);
a[!left] <- v;
assert { permut_sub (at a 'L) a !left (k + 1) };
assert { permut_sub (at a 'L) a 0 (length a) };
......
......@@ -5,9 +5,9 @@
<prover id="0" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../binary_sort.mlw" expanded="true">
<theory name="BinarySort" sum="33d84656fa3e7f9d3142595581a9acee" expanded="true">
<theory name="BinarySort" sum="fdb3a37048a74a0a24a69ddbeedfed40" expanded="true">
<goal name="WP_parameter occ_shift" expl="VC for occ_shift" expanded="true">
<transf name="split_goal_wp" expanded="true">
<transf name="split_goal_wp">
<goal name="WP_parameter occ_shift.1" expl="1. assertion">
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
......@@ -17,7 +17,7 @@
<goal name="WP_parameter occ_shift.3" expl="3. assertion">
<proof prover="1"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="WP_parameter occ_shift.4" expl="4. postcondition" expanded="true">
<goal name="WP_parameter occ_shift.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter occ_shift.5" expl="5. loop invariant init">
......@@ -32,7 +32,7 @@
<goal name="WP_parameter occ_shift.8" expl="8. assertion">
<proof prover="0"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="WP_parameter occ_shift.9" expl="9. assertion" expanded="true">
<goal name="WP_parameter occ_shift.9" expl="9. assertion">
<proof prover="0"><result status="valid" time="0.50"/></proof>
</goal>
<goal name="WP_parameter occ_shift.10" expl="10. postcondition">
......@@ -96,67 +96,34 @@
<goal name="WP_parameter binary_sort.18" expl="18. loop variant decrease">
<proof prover="1"><result status="valid" time="0.02" steps="28"/></proof>
</goal>
<goal name="WP_parameter binary_sort.19" expl="19. index in array bounds">
<proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="WP_parameter binary_sort.20" expl="20. assertion">
<proof prover="1"><result status="valid" time="0.02" steps="76"/></proof>
</goal>
<goal name="WP_parameter binary_sort.21" expl="21. assertion">
<proof prover="1"><result status="valid" time="0.01" steps="23"/></proof>
</goal>
<goal name="WP_parameter binary_sort.22" expl="22. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.07" steps="43"/></proof>
</goal>
<goal name="WP_parameter binary_sort.23" expl="23. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="66"/></proof>
</goal>
<goal name="WP_parameter binary_sort.24" expl="24. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter binary_sort.25" expl="25. type invariant">
<proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
<goal name="WP_parameter binary_sort.19" expl="19. precondition">
<proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="WP_parameter binary_sort.26" expl="26. index in array bounds">
<proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
</goal>
<goal name="WP_parameter binary_sort.27" expl="27. index in array bounds">
<proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="WP_parameter binary_sort.28" expl="28. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="40"/></proof>
</goal>
<goal name="WP_parameter binary_sort.29" expl="29. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="28"/></proof>
</goal>
<goal name="WP_parameter binary_sort.30" expl="30. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="27"/></proof>
</goal>
<goal name="WP_parameter binary_sort.31" expl="31. type invariant">
<proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
<goal name="WP_parameter binary_sort.20" expl="20. precondition">
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter binary_sort.32" expl="32. index in array bounds">
<proof prover="1"><result status="valid" time="0.02" steps="12"/></proof>
<goal name="WP_parameter binary_sort.21" expl="21. index in array bounds">
<proof prover="1"><result status="valid" time="0.00" steps="15"/></proof>
</goal>
<goal name="WP_parameter binary_sort.33" expl="33. assertion">
<proof prover="1"><result status="valid" time="1.84" steps="186"/></proof>
<goal name="WP_parameter binary_sort.22" expl="22. assertion">
<proof prover="1"><result status="valid" time="0.57" steps="174"/></proof>
</goal>
<goal name="WP_parameter binary_sort.34" expl="34. assertion">
<proof prover="1"><result status="valid" time="0.01" steps="23"/></proof>
<goal name="WP_parameter binary_sort.23" expl="23. assertion">
<proof prover="1"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
<goal name="WP_parameter binary_sort.35" expl="35. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.12" steps="198"/></proof>
<goal name="WP_parameter binary_sort.24" expl="24. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.12" steps="203"/></proof>
</goal>
<goal name="WP_parameter binary_sort.36" expl="36. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="62"/></proof>
<goal name="WP_parameter binary_sort.25" expl="25. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="65"/></proof>
</goal>
<goal name="WP_parameter binary_sort.37" expl="37. type invariant">
<goal name="WP_parameter binary_sort.26" expl="26. type invariant">
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="WP_parameter binary_sort.38" expl="38. postcondition">
<goal name="WP_parameter binary_sort.27" expl="27. postcondition">
<proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="WP_parameter binary_sort.39" expl="39. postcondition">
<goal name="WP_parameter binary_sort.28" expl="28. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
</transf>
......
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