new example: cubic root

parent 25247f43
module CubicRoot
use import int.Int
use import ref.Ref
function cube (x: int) : int = x * x * x
let cubic_root (x: int) : int
requires { x >= 0 }
ensures { cube (result - 1) <= x < cube result }
=
let a = ref 1 in
let b = ref 1 in
let y = ref 1 in
while !y <= x do
invariant { cube (!b - 1) <= x }
invariant { !y = cube !b }
invariant { !a = !b * !b }
variant { x - !y }
y := !y + 3 * !a + 3 * !b + 1;
a := !a + 2 * !b + 1;
b := !b + 1
done;
!b
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.4.0" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../cubic_root.mlw" expanded="true">
<theory name="CubicRoot" sum="7ca1d5866200b8590943317a70148ff0" expanded="true">
<goal name="WP_parameter cubic_root" expl="VC for cubic_root" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter cubic_root.1" expl="1. loop invariant init" expanded="true">
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="WP_parameter cubic_root.2" expl="2. loop invariant init" expanded="true">
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="WP_parameter cubic_root.3" expl="3. loop invariant init" expanded="true">
<proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="WP_parameter cubic_root.4" expl="4. loop invariant preservation" expanded="true">
<proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter cubic_root.5" expl="5. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter cubic_root.6" expl="6. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter cubic_root.7" expl="7. loop variant decrease" expanded="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter cubic_root.8" expl="8. postcondition" expanded="true">
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
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