COMPX554代写、代做Python编程设计、Java，c++语言代写

日期：2020-09-03 10:18

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