Prerequisites: CS 5423 , SWE 6623, and SWE 6613 recommended
3-0-3
The course is concerned with formal representation of the specification of software. Formal mechanisms for specifying, validating, and verifying software systems will be introduced to check for completeness and correctness as well as to discover ambiguities in the specifications. Both Propositional and Predicate Calculus will be reviewed and utilized to represent and reason about software specifications. Proof techniques and formal specification languages Z and the Object Constraint Language (OCL) will be explored.