A second-year bachelor CS course aimed at covering different aspects of software specification.
Z and Alloy are used for modeling the functionality aspect of software specification (as formal addenda to UML Class Diagrams). Sequence Diagrams (Message Sequence Charts) and State Diagrams (Statecharts) are other means taught in this course to capture the behavioral aspects of software specification.