bankAccount_M2_deposit.bum

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" version="5">
<org.eventb.core.event name="'" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION">
<org.eventb.core.action name="'" org.eventb.core.assignment="balance ≔ ∅" org.eventb.core.label="initBalance"/>
<org.eventb.core.action name="(" org.eventb.core.assignment="owner ≔ ∅" org.eventb.core.label="initOwner"/>
</org.eventb.core.event>
<org.eventb.core.seesContext name="(" org.eventb.core.target="bankAccount_C0"/>
<org.eventb.core.refinesMachine name=")" org.eventb.core.target="bankAccount_M1_accountCreation"/>
<org.eventb.core.event name="*" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="accountCreation">
<org.eventb.core.parameter name="'" org.eventb.core.identifier="c"/>
<org.eventb.core.guard name="(" org.eventb.core.label="inClient" org.eventb.core.predicate="c ∈ CLIENT"/>
<org.eventb.core.action name=")" org.eventb.core.assignment="owner ≔ owner ∪ {a ↦ c}" org.eventb.core.label="setNewAccountOwnership"/>
<org.eventb.core.action name="*" org.eventb.core.assignment="balance ≔ balance ∪ {a ↦ 0}" org.eventb.core.label="setNewAccountBalance"/>
<org.eventb.core.parameter name="+" org.eventb.core.identifier="a"/>
<org.eventb.core.guard name="," org.eventb.core.label="inAccount" org.eventb.core.predicate="a ∈ ACCOUNT"/>
<org.eventb.core.guard name="-" org.eventb.core.label="notRepeatedOwnership" org.eventb.core.predicate="a ∉ dom(owner)"/>
<org.eventb.core.guard name="." org.eventb.core.label="notRepeatedBalance" org.eventb.core.predicate="a ∉ dom(balance)"/>
<org.eventb.core.refinesEvent name="/" org.eventb.core.target="accountCreation"/>
</org.eventb.core.event>
<org.eventb.core.variable name="+" org.eventb.core.identifier="owner"/>
<org.eventb.core.variable name="," org.eventb.core.identifier="balance"/>
<org.eventb.core.invariant name="-" org.eventb.core.label="invBalance" org.eventb.core.predicate="balance ∈ ACCOUNT ⇸ ℕ"/>
<org.eventb.core.invariant name="." org.eventb.core.label="invOwner" org.eventb.core.predicate="owner ∈ ACCOUNT ⇸ CLIENT"/>
<org.eventb.core.event name="/" org.eventb.core.comment="FUN6: The deposit event effectively increases the balance of ACCOUNT a by x, no matter who the owner is" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="deposit">
<org.eventb.core.action name="'" org.eventb.core.assignment="balance ≔ balance  {a ↦ (balance(a) + x)}" org.eventb.core.label="updateBalance"/>
<org.eventb.core.guard name="(" org.eventb.core.label="inAccount" org.eventb.core.predicate="a ∈ ACCOUNT"/>
<org.eventb.core.parameter name=")" org.eventb.core.identifier="a"/>
<org.eventb.core.parameter name="+" org.eventb.core.identifier="x"/>
<org.eventb.core.guard name="," org.eventb.core.label="existingAccountOwner" org.eventb.core.predicate="a ∈ dom(owner)"/>
<org.eventb.core.guard name="-" org.eventb.core.label="existingAccountBalance" org.eventb.core.predicate="a ∈ dom(balance)"/>
<org.eventb.core.guard name="." org.eventb.core.label="amountIsPositive" org.eventb.core.predicate="x &gt; 0"/>
<org.eventb.core.refinesEvent name="/" org.eventb.core.target="operate"/>
</org.eventb.core.event>
<org.eventb.core.event name="0" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="operate">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="operate"/>
<org.eventb.core.action name="act1" org.eventb.core.assignment="balance :∈ ACCOUNT ⇸ ℕ" org.eventb.core.label="setNewAccountBalance"/>
<org.eventb.core.action name="act2" org.eventb.core.assignment="owner :∈ ACCOUNT ⇸ CLIENT" org.eventb.core.label="setNewAccountOwnership"/>
</org.eventb.core.event>
</org.eventb.core.machineFile>