B Assignment 1
Ken Robinson 26 February 2012
Name of assignment: ass1
Due date: March 4 2012
Assessment: 5 marks
Submission: give cs2111 ass1 CoffeeClub.zip
1 Overview
Important: please read
This assignment is intended to help you become familiar with:
• Event-B symbols,
• using Rodin,
• creating projects and machines,
• entering information into the bodies of machines
. This should help you become familiar with a number of functions of the Rodin toolkit. The marked up machines are appended to this specification. They are presented in the ISO characters used in the toolkit; some of those characters must be entered using ASCII representations.
Please see bonus requirement.
2 Requirement
A specification of machine CoffeeClub, context Members, and machine MemberShip, as discussed in the lectures, is required. You must carry out the actions described in the following section.
What you have to do
Please read and follow the instructions carefully.
Create a new development directory You can call it what you want, but for the purposes of this specification, it will be called CoffeeClub.
Run Rodin toolkit and create or load a workshpace.
Use the Event-B explorer to create a project called CoffeeClub.
浙大学霸代写 加微信 cstutorcs
4. Within the CoffeeClub project create the machine CoffeeClub.
5. Fix any errors and check the proof obligations in Event-B explorer.
6. Create the context Members and the machine MemberShip.
7. Please note that, where appropriate, the listing of refined events is shown with status ex- tended.
8. Export (File menu) a zip archive of the CoffeeClub project.
9. Submit assignment as above.
3.1 Requirements
The following is an abbreviated set of requirements.
REQ1 money bank for storing finite, non-negative funds
REQ2 an operation for adding money to the money bank
REQ3 an operation for removing money from the money bank.
REQ4 a facility for members to join the coffee club;
each member has a distinct membership id
REQ5 members have an account that cannot go into debt;
REQ6 an operation that enables a member to add money to their account;
REQ7 money added to a members account is also added to the club money bank;
REQ8 an operation that sets the price for a cup of coffee;
REQ9 an operation that enables a member to buy a cup of coffee;
the member’s account is reduced by the cost of a cup of coffee.
4 CoffeeClub Machine
machine CoffeeClub variables
piggybank REQ1 invariants
inv1: piggybank ∈ N events
Initialisation =b then
act1: piggybank := 0
REQ1: piggybank must be non-negative
initialise piggybank to satisfy inv1
FeedBank =b any
RobBank =b any
grd1: grd2:
amount ∈ N1
piggybank := piggybank + amount
amount ∈ N1 amount ≤ piggybank
There must be enough in the piggybank piggybank := piggybank − amount
4.1 Context Members
contextMembers sets
axm1: finite(MEMBER) REQ3: a finite set of members end
4.2 MemberShip Machine (Refinement)
machine MemberShip
Requirements:
REQ4, REQ5, REQ6, REQ7, REQ8, REQ9
CoffeeClub
piggybank members accounts coffeeprice
invariants
REQ4: the set of current members REQ5: the member accounts REQ8: the price of a cup of coffee
piggybank ∈ N
members ⊆ MEMBER accounts ∈ members → N coffeeprice ∈ N1
inv1: inv2: inv3: inv4:
Initialisation : extended =b then
REQ4: each member has unique id REQ5: each member has an account REQ8: any price other than free!
act2: act3: act4:
members := ∅ accounts := ∅ coffeeprice :∈ N1
empty set of members
empty set of accounts
initial coffee price set to arbitrary non-zero value
SetPrice =b any
CS Help, Email: tutorcs@163.com
grd1: amount ∈ N1 then
act1: coffeeprice := amount end
NewMember =b any
act1: act2:
REQ4, REQ5
Contribute =b
grd1: grd2:
act1: act2:
BuyCoffee =b any
grd1: grd2:
member ∈ MEMBER \ members members := members ∪ {member}
accounts(member) := 0
choose a unique member id
amount ∈ N1 member ∈ members
piggybank := piggybank + amount accounts(member) := accounts(member) + amount
member ∈ members accounts(member) ≥ coffeeprice
accounts(member) := accounts(member) − coffeeprice
FeedBank : extended =b
RobBank : extended =b
where then end
Programming Help, Add QQ: 749389476