Software Engineering using Formal Methods | |
Exercises Week 7 - Verification | |
Recommended2, 3, 4, 5, the Verification exercises from the 2 trial exams. You can download the Java sources for the exercises here. Exercise 1Consider the following scenario :A bank offers its customers certain services at the bank's numerous automated service terminals. Using the card and a PIN, the customer can check the balance of his account, he can withdraw cash and he can initiate a mailing of a printed account statement. If a wrong PIN is given 3 times in a row then the card is confiscated by the service terminal. A withdrawal of cash may not be larger than the current balance of the account and in any case may not exceed 1000 euros per day. This can obviously be enforced if the respective ATM is online. If an ATM cannot establish a connection to the bank, an offline cash withdrawal without check of the balance is made. The sum of all offline withdrawals until the balance can be checked and adjusted may never exceed 1000 euros, regardless of the number of days. There may be more than one card for each account. Issue of cards and opening of accounts is done with the central host. The cards themselves contain no software, but are basically data containers. It is possible to receive a written account statement for free once a month. Adjust the settings in KeY under Proof Search Strategy as following:
Exercise 2What does the following method do, assuming that x is a positive integer ? public int x; public int method() { int y = x; int z = 0; while (y > 0) { z = z + x; y = y - 1; } return z; }
Exercise 3What does the following method do, assuming that x is a positive integer and y is a strictly positive integer? public int x; public int y; public int method() { int x1 = x, q = 0; while (x1 >= y) { x1 = x1 - y; q = q + 1; } return q; }
Exercise 4Verify that method replaceIfGreater of class ArrayHelper in directory verify ensures its postconditions. Explain how you can read from the open goal(s) and the path to an open goal, what is going on. Fix then the bug in the specification or implementation and verify the method again.Exercise 5The directory verify contains a few classes. One of them is the class Person. Imagine the class belongs to a database of the authority responsible for issuing driver licenses. Further each person in this database has already successfully passed all tests. So each person has already a driver license, but some are still not old enough to actually be allowed to drive. You need to have fulfilled your 18th year to get the allowance. The allowance is issued by activating the license of a person.
| |
Home | Schedule | Exercises | Labs | Exam | Links | Course |