Parte 2

Untitled

The requirement is not verifiable because the term "annoying" is subjective and can take on different meanings for different users, so it doesn't provide an objective meaure that can be tested.

A verifiable version of this requirement could be "The OS should complete the start-up procedure in less than 20 seconds on a computer with at least the recoomended system requirements".

Untitled

We could keep 8 hours as an acceptable reminder period, a time in which there is time to take action even for commitments that require a lot of it, such as a flight.

However, given that "early enough" and "too early" are termis that have subjective interpretations and depend of specific events, the program should allow the user to choose how soon to receive the reminder, starting from a minimum of 10 minutes up to a maximum of 24 hours before the event.

Untitled

The first approach has a high degree of pessimistic inaccuracy, therefore it tends to be more pessimistic than the actual precision, making the system generally more safe, and garantees serializability. This approach simplifies the concept of atomic transactions, and therefore it becomes very simpmle to verify manually or automatically. The cost of these benefits are the performances.

The second option has a degree of both pessimistic and optimistic inaccuracy: while it can verify finer-grain locking, they can still reject methods that ensure serializability. The property of atomic transaction is not simplified as much as in the first option.

Requiring the progrmamer to adhere to a specific concurrency control protocol can be a compromise between pessimistic and optimistic inaccuracy: it simplifies the property to a certain extent, but still requires manual work in writing / verifying the code. Still, it provides a balance between performance and correctness.

The last option represents optimistic inaccuracy. It allows the possibility of serializability without locking but relies on the "happens before" relation among transactions. The property isn't simplified, but is substituted with another (acyclicity of the graph), which might not be straightforward to verify.