Skip to content
GitLab
Commit 152389f2 authored by fmeirim's avatar fmeirim
Browse files

Added dependency analysis

parent 16f6f76a
Expand all Hide whitespace changes
Inline Side-by-side
bin/why3cise.opt
View file @ 152389f2
No preview for this file type
src/core/.#term.ml 0 → 120000
View file @ 152389f2
filipemeirim@MBP-de-Filipe.Home.3114
\ No newline at end of file
src/tools/bank.mlw
View file @ 152389f2
......@@ -12,21 +12,23 @@ type state [@state]= {
invariant{forall i: int. i >= 0 /\ i < length balances -> balances[i] >= 0}
by {balances = make 0 0}
let deposit(accountId amount: int) (state : state): unit
let ghost deposit(accountId amount: int) (state : state): unit
writes{state.balances}
requires{amount > 0}
requires {accountId >= 0 /\ accountId < length state.balances}
ensures {state.balances[accountId] = old(state.balances)[accountId] + amount}
ensures {state.balances[accountId] = (old(state.balances)[accountId]) + amount}
ensures {forall i: int. i <> accountId -> state.balances[i] = (old state.balances)[i]}
= state.balances[accountId] <- state.balances[accountId] + amount
ensures {length (state.balances) = length (old state.balances)}
= state.balances[accountId] <- (state.balances[accountId]) + amount
let withdraw(accountId amount: int) (state : state) : unit
let ghost withdraw(accountId amount: int) (state : state) : unit
writes{state.balances}
requires {amount > 0}
requires {state.balances[accountId] - amount >= 0}
requires {accountId >= 0 /\ accountId < length state.balances}
ensures {state.balances[accountId] = old(state.balances)[accountId] - amount}
ensures {forall i: int. i <> accountId -> state.balances[i] = (old state.balances)[i]}
ensures {length (state.balances) = length (old state.balances)}
= state.balances[accountId] <- state.balances[accountId] - amount
let ghost predicate state_equality [@state_eq] (s1 s2 : state)
......
src/tools/bank/why3session.xml
View file @ 152389f2
......@@ -3,9 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="0" name="Z3" version="4.8.4" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Z3" version="4.8.4" alternative="counterexamples" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.6" alternative="counterexamples" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<file proved="true">
<path name=".."/>
......@@ -16,36 +14,61 @@
<proof prover="4"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC deposit" expl="VC for deposit" proved="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.05"/></proof>
<proof prover="2" obsolete="true"><result status="unknown" time="0.03"/></proof>
<proof prover="4"><result status="valid" time="0.05"/></proof>
<transf name="split_vc" >
<goal name="VC deposit.0" expl="index in array bounds">
<proof prover="4" obsolete="true"><result status="valid" time="0.03"/></proof>
<goal name="VC deposit.0" expl="index in array bounds" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC deposit.1" expl="index in array bounds">
<proof prover="4" obsolete="true"><result status="valid" time="0.03"/></proof>
<goal name="VC deposit.1" expl="index in array bounds" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC deposit.2" expl="type invariant">
<proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="unknown" time="2.68"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.01" steps="30"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="4" obsolete="true"><result status="valid" time="0.03"/></proof>
<proof prover="0"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="highfailure" time="0.00"/></proof>
<proof prover="4"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC deposit.3" expl="postcondition">
<proof prover="2" obsolete="true"><result status="valid" time="0.00" steps="14"/></proof>
<proof prover="4" obsolete="true"><result status="valid" time="0.02"/></proof>
<proof prover="0"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="highfailure" time="0.00"/></proof>
<proof prover="4"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC deposit.4" expl="postcondition">
<proof prover="2" obsolete="true"><result status="valid" time="0.01" steps="18"/></proof>
<proof prover="4" obsolete="true"><result status="valid" time="0.03"/></proof>
<proof prover="0"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="highfailure" time="0.00"/></proof>
<proof prover="4"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC deposit.5" expl="postcondition">
</goal>
</transf>
</goal>
<goal name="VC withdraw" expl="VC for withdraw" proved="true">
<proof prover="2" obsolete="true"><result status="valid" time="0.01" steps="53"/></proof>
<proof prover="4"><result status="valid" time="0.05"/></proof>
<transf name="split_vc" >
<goal name="VC withdraw.0" expl="index in array bounds" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC withdraw.1" expl="index in array bounds" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC withdraw.2" expl="type invariant">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="highfailure" time="0.00"/></proof>
<proof prover="4"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC withdraw.3" expl="postcondition">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="highfailure" time="0.00"/></proof>
<proof prover="4"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC withdraw.4" expl="postcondition">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="highfailure" time="0.00"/></proof>
<proof prover="4"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC withdraw.5" expl="postcondition">
</goal>
</transf>
</goal>
</theory>
</file>
......
src/tools/bank__cise.mlw
View file @ 152389f2
......@@ -71,5 +71,43 @@ module CiseAnalysis
accountId2 >= 0 /\ accountId2 < length (balances state2) };
deposit accountId1 amount1 state1;
deposit accountId2 amount2 state1
let ghost withdraw_deposit_dependency (ghost _:()) : () =
let ghost accountId1 = any int in
let ghost amount1 = any int in
let ghost state1 = any state in
let ghost accountId2 = any int in
let ghost amount2 = any int in
let ghost state2 = any state
in
assume { (amount1 > 0 /\
accountId1 >= 0 /\ accountId1 < length (balances state1)) /\
state_equality state1 state2 };
deposit accountId1 amount1 state1;
assume { amount2 > 0 /\
((balances state1)[accountId2] - amount2) >= 0 /\
accountId2 >= 0 /\ accountId2 < length (balances state1) };
withdraw accountId2 amount2 state2
let ghost deposit_withdraw_dependency (ghost _:()) : () =
let ghost accountId1 = any int in
let ghost amount1 = any int in
let ghost state1 = any state in
let ghost accountId2 = any int in
let ghost amount2 = any int in
let ghost state2 = any state
in
assume { (amount1 > 0 /\
((balances state1)[accountId1] - amount1) >= 0 /\
accountId1 >= 0 /\ accountId1 < length (balances state1)) /\
state_equality state1 state2 };
withdraw accountId1 amount1 state1;
assume { amount2 > 0 /\
accountId2 >= 0 /\ accountId2 < length (balances state1) };
deposit accountId2 amount2 state2
end
src/tools/bank__cise/why3session.xml 0 → 100644
View file @ 152389f2
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="0" name="Z3" version="4.8.4" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<file>
<path name=".."/>
<path name="bank__cise.mlw"/>
<theory name="CiseAnalysis">
<goal name="VC deposit_withdraw_commutativity" expl="VC for deposit_withdraw_commutativity" proved="true">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="highfailure" time="0.00"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
<transf name="split_vc" proved="true" >
<goal name="VC deposit_withdraw_commutativity.0" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC deposit_withdraw_commutativity.1" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC deposit_withdraw_commutativity.2" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC deposit_withdraw_commutativity.3" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC deposit_withdraw_commutativity.4" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC deposit_withdraw_commutativity.5" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC deposit_withdraw_commutativity.6" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC deposit_withdraw_commutativity.7" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC deposit_withdraw_commutativity.8" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC deposit_withdraw_commutativity.9" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC deposit_withdraw_commutativity.10" expl="postcondition" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="highfailure" time="0.00"/></proof>
<proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
<transf name="unfold" proved="true" arg1="state_equality">
<goal name="VC deposit_withdraw_commutativity.10.0" expl="VC for deposit_withdraw_commutativity" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="highfailure" time="0.00"/></proof>
<proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
<transf name="unfold" proved="true" arg1="array_eq">
<goal name="VC deposit_withdraw_commutativity.10.0.0" expl="VC for deposit_withdraw_commutativity" proved="true">
<proof prover="2"><result status="valid" time="0.11"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC withdraw_stability" expl="VC for withdraw_stability">
</goal>
<goal name="VC deposit_stability" expl="VC for deposit_stability" proved="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.28"/></proof>
<proof prover="1" obsolete="true"><result status="highfailure" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<transf name="split_vc" proved="true" >
<goal name="VC deposit_stability.0" expl="precondition" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="highfailure" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC deposit_stability.1" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC deposit_stability.2" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC deposit_stability.3" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
<goal name="VC deposit_withdraw_dependency" expl="VC for deposit_withdraw_dependency" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
<transf name="split_vc" >
<goal name="VC deposit_withdraw_dependency.0" expl="precondition">
<proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC deposit_withdraw_dependency.1" expl="precondition">
<proof prover="0" obsolete="true"><result status="unknown" time="0.73"/></proof>
<proof prover="1" obsolete="true"><result status="highfailure" time="0.00"/></proof>
<proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC deposit_withdraw_dependency.2" expl="precondition">
<proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC deposit_withdraw_dependency.3" expl="precondition">
<proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC deposit_withdraw_dependency.4" expl="precondition">
<transf name="split_vc" >
<goal name="VC deposit_withdraw_dependency.4.0" expl="precondition">
<proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC deposit_withdraw_dependency.4.1" expl="precondition">
<proof prover="2" obsolete="true"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC withdraw_deposit_dependency" expl="VC for withdraw_deposit_dependency">
<proof prover="0"><result status="unknown" time="0.69"/></proof>
<proof prover="1"><result status="highfailure" time="0.00"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
</goal>
</theory>
</file>
</why3session>
src/tools/lines.txt 0 → 100644
View file @ 152389f2
token deposit t1
token withdraw t2
src/why3cise/why3cise.ml
View file @ 152389f2
This diff is collapsed.
Supports Markdown
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