-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathbankAccount_M3_withdraw.bcm
68 lines (68 loc) · 17.4 KB
/
bankAccount_M3_withdraw.bcm
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.scMachineFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd">
<org.eventb.core.scRefinesMachine name="'" org.eventb.core.scTarget="/BankAccount/bankAccount_M2_deposit.bcm" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.refinesMachine#)"/>
<org.eventb.core.scSeesContext name="(" org.eventb.core.scTarget="/BankAccount/bankAccount_C0.bcc" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.seesContext#("/>
<org.eventb.core.scInternalContext name="bankAccount_C0">
<org.eventb.core.scAxiom name="'" org.eventb.core.label="axm1" org.eventb.core.predicate="finite(ACCOUNT)" org.eventb.core.source="/BankAccount/bankAccount_C0.buc|org.eventb.core.contextFile#bankAccount_C0|org.eventb.core.axiom#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="(" org.eventb.core.label="axm2" org.eventb.core.predicate="finite(CLIENT)" org.eventb.core.source="/BankAccount/bankAccount_C0.buc|org.eventb.core.contextFile#bankAccount_C0|org.eventb.core.axiom#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name=")" org.eventb.core.label="axm3" org.eventb.core.predicate="K∈ℕ" org.eventb.core.source="/BankAccount/bankAccount_C0.buc|org.eventb.core.contextFile#bankAccount_C0|org.eventb.core.axiom#," org.eventb.core.theorem="false"/>
<org.eventb.core.scCarrierSet name="ACCOUNT" org.eventb.core.source="/BankAccount/bankAccount_C0.buc|org.eventb.core.contextFile#bankAccount_C0|org.eventb.core.carrierSet#'" org.eventb.core.type="ℙ(ACCOUNT)"/>
<org.eventb.core.scCarrierSet name="CLIENT" org.eventb.core.source="/BankAccount/bankAccount_C0.buc|org.eventb.core.contextFile#bankAccount_C0|org.eventb.core.carrierSet#(" org.eventb.core.type="ℙ(CLIENT)"/>
<org.eventb.core.scConstant name="K" org.eventb.core.source="/BankAccount/bankAccount_C0.buc|org.eventb.core.contextFile#bankAccount_C0|org.eventb.core.constant#+" org.eventb.core.type="ℤ"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInvariant name="bankAccount_C1" org.eventb.core.label="invBalance" org.eventb.core.predicate="balance∈ACCOUNT ⇸ ℕ" org.eventb.core.source="/BankAccount/bankAccount_M0.bum|org.eventb.core.machineFile#bankAccount_M0|org.eventb.core.invariant#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="bankAccount_C2" org.eventb.core.label="invOwner" org.eventb.core.predicate="owner∈ACCOUNT ⇸ CLIENT" org.eventb.core.source="/BankAccount/bankAccount_M0.bum|org.eventb.core.machineFile#bankAccount_M0|org.eventb.core.invariant#," org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="bankAccount_C3" org.eventb.core.label="invBalance" org.eventb.core.predicate="balance∈ACCOUNT ⇸ ℕ" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.invariant#-" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="bankAccount_C4" org.eventb.core.label="invOwner" org.eventb.core.predicate="owner∈ACCOUNT ⇸ CLIENT" org.eventb.core.source="/BankAccount/bankAccount_M1_accountCreation.bum|org.eventb.core.machineFile#bankAccount_M1_accountCreation|org.eventb.core.invariant#." org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="bankAccount_C5" org.eventb.core.label="invBalance" org.eventb.core.predicate="balance∈ACCOUNT ⇸ ℕ" org.eventb.core.source="/BankAccount/bankAccount_M2_deposit.bum|org.eventb.core.machineFile#bankAccount_M2_deposit|org.eventb.core.invariant#-" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="bankAccount_C6" org.eventb.core.label="invOwner" org.eventb.core.predicate="owner∈ACCOUNT ⇸ CLIENT" org.eventb.core.source="/BankAccount/bankAccount_M2_deposit.bum|org.eventb.core.machineFile#bankAccount_M2_deposit|org.eventb.core.invariant#." org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="bankAccount_C7" org.eventb.core.label="invBalance" org.eventb.core.predicate="balance∈ACCOUNT ⇸ ℕ" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.invariant#-" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="bankAccount_C8" org.eventb.core.label="invOwner" org.eventb.core.predicate="owner∈ACCOUNT ⇸ CLIENT" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.invariant#." org.eventb.core.theorem="false"/>
<org.eventb.core.scVariable name="balance" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.variable#," org.eventb.core.type="ℙ(ACCOUNT×ℤ)"/>
<org.eventb.core.scVariable name="owner" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.variable#+" org.eventb.core.type="ℙ(ACCOUNT×CLIENT)"/>
<org.eventb.core.scEvent name="bankAccount_C9" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#'">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/BankAccount/bankAccount_M2_deposit.bcm|org.eventb.core.scMachineFile#bankAccount_M2_deposit|org.eventb.core.scEvent#bankAccount_C7" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#'"/>
<org.eventb.core.scAction name="(" org.eventb.core.assignment="balance ≔ ∅ ⦂ ℙ(ACCOUNT×ℤ)" org.eventb.core.label="initBalance" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#'|org.eventb.core.action#'"/>
<org.eventb.core.scAction name=")" org.eventb.core.assignment="owner ≔ ∅ ⦂ ℙ(ACCOUNT×CLIENT)" org.eventb.core.label="initOwner" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#'|org.eventb.core.action#("/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="bankAccount_C:" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="accountCreation" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#*">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/BankAccount/bankAccount_M2_deposit.bcm|org.eventb.core.scMachineFile#bankAccount_M2_deposit|org.eventb.core.scEvent#bankAccount_C8" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#*|org.eventb.core.refinesEvent#\/"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="inClient" org.eventb.core.predicate="c∈CLIENT" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#*|org.eventb.core.guard#(" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="inAccount" org.eventb.core.predicate="a∈ACCOUNT" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#*|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="notRepeatedOwnership" org.eventb.core.predicate="a∉dom(owner)" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#*|org.eventb.core.guard#-" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="notRepeatedBalance" org.eventb.core.predicate="a∉dom(balance)" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#*|org.eventb.core.guard#." org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="a" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#*|org.eventb.core.parameter#+" org.eventb.core.type="ACCOUNT"/>
<org.eventb.core.scParameter name="c" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#*|org.eventb.core.parameter#'" org.eventb.core.type="CLIENT"/>
<org.eventb.core.scAction name="d" org.eventb.core.assignment="owner ≔ owner∪{a ↦ c}" org.eventb.core.label="setNewAccountOwnership" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#*|org.eventb.core.action#)"/>
<org.eventb.core.scAction name="e" org.eventb.core.assignment="balance ≔ balance∪{a ↦ 0}" org.eventb.core.label="setNewAccountBalance" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#*|org.eventb.core.action#*"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="bankAccount_C;" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="deposit" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#\/">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/BankAccount/bankAccount_M2_deposit.bcm|org.eventb.core.scMachineFile#bankAccount_M2_deposit|org.eventb.core.scEvent#bankAccount_C9" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#\/|org.eventb.core.refinesEvent#\/"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="inAccount" org.eventb.core.predicate="a∈ACCOUNT" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#\/|org.eventb.core.guard#(" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="existingAccountOwner" org.eventb.core.predicate="a∈dom(owner)" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#\/|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="existingAccountBalance" org.eventb.core.predicate="a∈dom(balance)" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#\/|org.eventb.core.guard#-" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="amountIsPositive" org.eventb.core.predicate="x>0" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#\/|org.eventb.core.guard#." org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="a" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#\/|org.eventb.core.parameter#)" org.eventb.core.type="ACCOUNT"/>
<org.eventb.core.scParameter name="x" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#\/|org.eventb.core.parameter#+" org.eventb.core.type="ℤ"/>
<org.eventb.core.scAction name="y" org.eventb.core.assignment="balance ≔ balance{a ↦ balance(a)+x}" org.eventb.core.label="updateBalance" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#\/|org.eventb.core.action#'"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="bankAccount_C=" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="withdraw" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#0">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/BankAccount/bankAccount_M2_deposit.bcm|org.eventb.core.scMachineFile#bankAccount_M2_deposit|org.eventb.core.scEvent#bankAccount_C:" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#0|org.eventb.core.refinesEvent#grd3"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="inClient" org.eventb.core.predicate="c∈CLIENT" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#0|org.eventb.core.guard#'" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="inAccount" org.eventb.core.predicate="a∈ACCOUNT" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#0|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="existingAccountOwner" org.eventb.core.predicate="a∈dom(owner)" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#0|org.eventb.core.guard#grd1" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="existingAccountBalance" org.eventb.core.predicate="a∈dom(balance)" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#0|org.eventb.core.guard#grd2" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="amountIsPositive" org.eventb.core.predicate="x>0" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#0|org.eventb.core.guard#-" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="-" org.eventb.core.label="clientIsOwner" org.eventb.core.predicate="c=owner(a)" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#0|org.eventb.core.guard#." org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="." org.eventb.core.label="balanceIsSufficient" org.eventb.core.predicate="balance(a)≥x" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#0|org.eventb.core.guard#\/" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="a" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#0|org.eventb.core.parameter#*" org.eventb.core.type="ACCOUNT"/>
<org.eventb.core.scParameter name="c" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#0|org.eventb.core.parameter#)" org.eventb.core.type="CLIENT"/>
<org.eventb.core.scParameter name="x" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#0|org.eventb.core.parameter#+" org.eventb.core.type="ℤ"/>
<org.eventb.core.scAction name="y" org.eventb.core.assignment="balance ≔ balance{a ↦ balance(a) − x}" org.eventb.core.label="updateBalance" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#0|org.eventb.core.action#("/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="bankAccount_C>" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="operate" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#1">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/BankAccount/bankAccount_M2_deposit.bcm|org.eventb.core.scMachineFile#bankAccount_M2_deposit|org.eventb.core.scEvent#bankAccount_C:" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#1|org.eventb.core.refinesEvent#("/>
<org.eventb.core.scAction name="(" org.eventb.core.assignment="balance :∈ ACCOUNT ⇸ ℕ" org.eventb.core.label="setNewAccountBalance" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#1|org.eventb.core.action#act1"/>
<org.eventb.core.scAction name=")" org.eventb.core.assignment="owner :∈ ACCOUNT ⇸ CLIENT" org.eventb.core.label="setNewAccountOwnership" org.eventb.core.source="/BankAccount/bankAccount_M3_withdraw.bum|org.eventb.core.machineFile#bankAccount_M3_withdraw|org.eventb.core.event#1|org.eventb.core.action#act2"/>
</org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>