Skip to content

GitLab

Commit 6d9c66b4 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

test of ceil function

parent f61e99e7
Hide whitespace changes
Inline Side-by-side
examples/tests-provers/ceil.why 0 → 100644
View file @ 6d9c66b4
theory Ceil
use import real.Real
use import real.RealInfix
use import real.Truncate
goal ceil_obvious: ceil 0.1 = 1
lemma unity:
forall b: real. b > 0.0 -> b = 1.0 *. b
lemma unity2:
forall b: real. b > 0.0 -> b /. b = (1.0 *. b) /. b
lemma perm_div:
forall a b:real. a > 0.0 /\ b > 0.0 -> (a *. b) /. b = a *. (b /. b)
lemma perm_div2:
forall a b:real. a > 0.0 /\ b > 0.0 -> a *. b /. b = a /. b *. b
lemma div_mult_perm:
forall b: real. b > 0.0 -> (1.0 /. b) *. b = (1.0 *. b) /. b
lemma b_div_b_is_one:
forall b: real. b > 0.0 -> 1.0 = b /. b
lemma inverse_inverse_is_same:
forall b: real. b > 0.0 -> 1.0 = (1.0 /. b) *. b
lemma inverse_bigger_zero:
forall b: real. b > 0.0 -> 1.0 /. b > 0.0
lemma div_equals_mult_w_inverse:
forall a b:real. b > 0.0 -> a /. b = a *. (1.0 /. b)
lemma mult_bigger_zero:
forall a b: real. a > 0.0 /\ b > 0.0 -> a *. b > 0.0
goal ceil_never_zero:
forall a b: real. a > 0.0 /\ b > 0.0 -> ceil (a /. b) <> 0
end
examples/tests-provers/ceil/why3session.xml 0 → 100644
View file @ 6d9c66b4
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="1"
name="Alt-Ergo"
version="0.95"/>
<prover
id="2"
name="CVC3"
version="2.2"/>
<prover
id="3"
name="CVC3"
version="2.4.1"/>
<prover
id="4"
name="Z3"
version="2.19"/>
<prover
id="5"
name="Z3"
version="3.2"/>
<prover
id="6"
name="Z3"
version="4.2"/>
<file
name="../ceil.why"
verified="true"
expanded="true">
<theory
name="Ceil"
locfile="../ceil.why"
loclnum="1" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
<goal
name="ceil_obvious"
locfile="../ceil.why"
loclnum="6" loccnumb="7" loccnume="19"
sum="49526ea2821e8c5d8d98d3fda2ed3620"
proved="true"
expanded="true"
shape="ainfix =aceilc0.1c1">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="unity"
locfile="../ceil.why"
loclnum="8" loccnumb="8" loccnume="13"
sum="83e246df0203d223db3aefeea911e5ca"
proved="true"
expanded="true"
shape="ainfix =V0ainfix *.c1.0V0Iainfix &gt;V0c0.0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="unity2"
locfile="../ceil.why"
loclnum="11" loccnumb="8" loccnume="14"
sum="6a645e9e1ee717bd4df95a3318083c3c"
proved="true"
expanded="true"
shape="ainfix =ainfix /.V0V0ainfix /.ainfix *.c1.0V0V0Iainfix &gt;V0c0.0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="perm_div"
locfile="../ceil.why"
loclnum="14" loccnumb="8" loccnume="16"
sum="d949fb1798189bda1fbf7cd1e62e06ac"
proved="true"
expanded="true"
shape="ainfix =ainfix /.ainfix *.V0V1V1ainfix *.V0ainfix /.V1V1Iainfix &gt;V1c0.0Aainfix &gt;V0c0.0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="perm_div2"
locfile="../ceil.why"
loclnum="17" loccnumb="8" loccnume="17"
sum="872f7e516c036f14e8c5f228a5a093b0"
proved="true"
expanded="true"
shape="ainfix =ainfix /.ainfix *.V0V1V1ainfix *.ainfix /.V0V1V1Iainfix &gt;V1c0.0Aainfix &gt;V0c0.0F">
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="div_mult_perm"
locfile="../ceil.why"
loclnum="20" loccnumb="8" loccnume="21"
sum="64d37d10f94221cdda1c2603e670e505"
proved="true"
expanded="true"
shape="ainfix =ainfix *.ainfix /.c1.0V0V0ainfix /.ainfix *.c1.0V0V0Iainfix &gt;V0c0.0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="b_div_b_is_one"
locfile="../ceil.why"
loclnum="23" loccnumb="8" loccnume="22"
sum="ae8bd6bcd64c57f3d58abe4b8f6cff18"
proved="true"
expanded="true"
shape="ainfix =c1.0ainfix /.V0V0Iainfix &gt;V0c0.0F">
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="inverse_inverse_is_same"
locfile="../ceil.why"
loclnum="26" loccnumb="8" loccnume="31"
sum="1e7431cf867c84c7f705f0170ec519b3"
proved="true"
expanded="true"
shape="ainfix =c1.0ainfix *.ainfix /.c1.0V0V0Iainfix &gt;V0c0.0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="inverse_bigger_zero"
locfile="../ceil.why"
loclnum="29" loccnumb="8" loccnume="27"
sum="413ddb1462a62e9dc7351da240bc534c"
proved="true"
expanded="true"
shape="ainfix &gt;ainfix /.c1.0V0c0.0Iainfix &gt;V0c0.0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="div_equals_mult_w_inverse"
locfile="../ceil.why"
loclnum="32" loccnumb="8" loccnume="33"
sum="474f333e20af5b5c795f9d2332ef5f34"
proved="true"
expanded="true"
shape="ainfix =ainfix /.V0V1ainfix *.V0ainfix /.c1.0V1Iainfix &gt;V1c0.0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="mult_bigger_zero"
locfile="../ceil.why"
loclnum="35" loccnumb="8" loccnume="24"
sum="83d5b29259f6af57da459896cf946c6a"
proved="true"
expanded="true"
shape="ainfix &gt;ainfix *.V0V1c0.0Iainfix &gt;V1c0.0Aainfix &gt;V0c0.0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>