COMPX554辅导、讲解Python编程设计、Java，c++语言辅导
讲解留学生Processing|讲解SPSS
Coursework Two
Investigating Models
NOTE: your answers to this coursework are due in to the 554 Moodle site by 1000 on
Monday 7th September 2020. The file you submit MUST be a PDF file produced using
LATEX.
1. Get a copy of the Z birthday book model from the Moodle site for the course. Make
sure that you can compile it (using LATEX) without any errors. The PDF of how it
should look is also on the Moodle site, so you can check you are getting the right
result.
2. Load your birthday book file into ProB. You will need to make sure that you select
the “Other Formalisms” item in the “Open” menu in order to see the file.
Make sure you get no syntax or type errors (the file I’ve given doesn’t contain any!).
Go to the “Preferences” menu in ProB and make sure that the “DEFAULT SETSIZE:
Size of unspecified deferred sets in SETS section” preference has value 2, the “MaxInt,
used for expressions such as xx::NAT (2147483647 for 4 byte ints)” has value
3 and the “MinInt, used for expressions such as xx::INT (-2147483648 for 4 byte
ints)” has value -1. (If you use larger numbers in these places then the models that
are possible get so huge that checking takes a very long time.)
3. Play with the model, i.e. add both the possible names with some choice of the
possible dates, reset, add names with different dates, keep playing until you are
happy you understand what is happening. Make sure you understand what each
operation you choose does, and why.
Note the information that ProB displays in the three panes at the bottom of its
window. See how the current state information is shown in “State Properties”, how
the operations that it is possible to perform (because their pre-conditions hold in
the current state) show up in “Enabled operations“ and how “History” shows you
what you have been doing. Also, use the arrows to go backwards and forwards
through the evolution of the model.
Finally, explore the “Help” menu, particularly the parts which tell you about Z.
4. Change AddBirthday by commenting out (which you do by starting the line with
%) the pre-condition (i.e. name? ∈/ known). Now see how the behaviour changes.
What happens that’s different if you add NAME1 at DATE1? Why is this?
5. Now change the type of birthday to a relation rather than (as it is now) a partial
function. See how the behaviour changes again. What happens now if you add
NAME1 at DATE1? Why is this? Why is the type of birthday as a partial function
so important?
1
6. Try uncommenting the pre-condition of AddBirthday. Run the experiments above
again. What does this tell you about the relation between partial functions and
relations and the pre-condition of AddBirthday?
7. Put back everything to how it was originally. Now add an operation RemoveBirthday
which, given a name, removes it from the book. Do you need a pre-condition for
this operation? If so, what is it, and why do you need it?
8. To see how model-checking works, add an invariant schema which checks that in
every state the birthday book relates at most one date to any name. That is
∀ b0, b1 : birthday • first b0 = first b1 ⇒ second b0 = second b1
What is the invariant schema?
9. Keeping the invariant schema, change the type of birthday to be a relation again,
and comment-out the pre-condition of AddBirthday. Now, run the model checker
again. You will get an error. Explain what the model-checker has found—use the
History to guide your explanation.
10. Keeping the type of birthday as a relation (but making sure that AddBirthday has its
pre-condition), add an operation UpdateName which allows the user to change the
name of someone already in the book Model check to see if there are any problems.
If there are, perhaps you need to add another pre-condition to UpdateName. Say
what it is, and why it works.
11. Add to the state schema so that the book can now also record addresses from the
set [ADDRESS]. Update the operations you have so far so that an address is also
added when an entry for someone’s birthday is made and deleted, and when a name
is updated too. Check the new system to see that no errors have been introduced.
What are your new schemas for the state and the updated operations?
12. Add error reporting in order to define total operations that correspond the (in
general) partial operations given so far.
Do this by adding a new type
Report ::= Ok | Error
and new schemas OK (which simply provides for an output of the value Ok from
the type Report) and schemas like
ErrorAdd
name? : NAME
ΞBirthdayBook
report! : Report
name? ∈ known
report! = Error
2
and
TotalAddBirthday = ( b AddBirthday ∧ OK) ∨ ErrorAdd
for each of the operations in questions 7 and 10.
13. Run all your checks to make sure that the total operations work as required.
14. Explain clearly how you can use ProB to explore, by animation, and see which
operations might be total, and which non-total ones are not.
3