| 1 |
Method signature is complete: operation name, parameter types, and return type |
Pass |
Each contract gives name, parameter list and return type (`startStudySession(): CardDto |
| 2 |
Preconditions explicitly list required state before execution |
Pass |
Preconditions are listed per contract. |
| 3 |
Postconditions explicitly describe resulting state using Larman's "instance created/associated/attribute modified" style |
Pass |
Postconditions use created / associated / destroyed / attribute set wording. |
| 4 |
Exceptions and error conditions are documented, including the triggering precondition failure |
Pass |
Each contract has an Exceptions table with the failing precondition. |
| 5 |
Operation is explicitly traceable to a single SSD message |
Pass |
Each of the four contracts (startStudySession, chooseLevel, markKnown, markUnknown) traces to exactly one SSD message; the timer step has none and says so. |
| 6 |
Contract avoids specifying implementation/algorithmic details (declarative, not procedural) |
Pass |
Postconditions are declarative. |
| 7 |
Cross-references the Domain Model classes/associations affected by pre/postconditions |
Pass |
Domain Model concepts and IT terms are cited per contract. |
