FoVeOOS challenge 2: simplified pattern macthing

parent 1060d7e5
......@@ -20,10 +20,10 @@ module MaximumTree
let rec maximum (t: tree) : int =
{ t <> Empty }
match t with
| Empty -> absurd
| Empty -> absurd
| Node Empty v Empty -> v
| Node Empty v r -> max v (maximum r)
| Node l v Empty -> max (maximum l) v
| Node Empty v s
| Node s v Empty -> max (maximum s) v
| Node l v r -> max (maximum l) (max v (maximum r))
end
{ mem result t /\ forall x: int. mem x t -> x <= result }
......
......@@ -45,16 +45,16 @@
<goal
name="WP_parameter maximum"
expl="parameter maximum"
sum="be2c72561ff37f3f52d7a3123788f957"
sum="f40fb156943f0b6bc126f4aa41b513f4"
proved="true"
expanded="true"
shape="CV0aEmptyfaNodeaEmptyVaEmptyainfix <=V2V1IamemV2V0FAamemV1V0aNodeaEmptyVVainfix <=V6amaxV3V5IamemV6V0FAamemamaxV3V5V0Iainfix <=V7V5IamemV7V4FAamemV5V4FAainfix =V4aEmptyNaNodeVVaEmptyainfix <=V11amaxV10V9IamemV11V0FAamemamaxV10V9V0Iainfix <=V12V10IamemV12V8FAamemV10V8FAainfix =V8aEmptyNaNodeVVVainfix <=V18amaxV16amaxV14V17IamemV18V0FAamemamaxV16amaxV14V17V0Iainfix <=V19V17IamemV19V15FAamemV17V15FAainfix =V15aEmptyNIainfix <=V20V16IamemV20V13FAamemV16V13FAainfix =V13aEmptyNIainfix =V0aEmptyNF">
shape="CV0aEmptyfaNodeaEmptyVaEmptyainfix <=V2V1IamemV2V0FAamemV1V0aNodeVVaEmptyOaNodeaEmptyVVainfix <=V6amaxV5V3IamemV6V0FAamemamaxV5V3V0Iainfix <=V7V5IamemV7V4FAamemV5V4FAainfix =V4aEmptyNaNodeVVVainfix <=V13amaxV11amaxV9V12IamemV13V0FAamemamaxV11amaxV9V12V0Iainfix <=V14V12IamemV14V10FAamemV12V10FAainfix =V10aEmptyNIainfix <=V15V11IamemV15V8FAamemV11V8FAainfix =V8aEmptyNIainfix =V0aEmptyNF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.36"/>
<result status="valid" time="0.40"/>
</proof>
</goal>
</theory>
......
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