Theory and Practice of Algebraic Specifications (P00904)

? Credit Points : 10 ? SCQF Level : 11 ? Acronym : INF-P-TPAS

The course presents an approach to formal specification, verification and formal development in some detail. Students will learn how to write specifications, what they mean, how to reason about them and how to use them in developing modular software systems. The emphasis will be split evenly between practice ("how to write and use specifications") and theory ("what they mean" etc.).

Entry Requirements

? Pre-requisites : PGs only or with permission of Director of Teaching.

Subject Areas

Home subject area

Software Engineering, (School of Informatics, Schedule O)

Other subject areas

Theoretical Computer Science, (School of Informatics, Schedule O)

Delivery Information

? Normal year taken : Postgraduate

? Delivery Period : Not being delivered

? Contact Teaching Time : 2 hour(s) per week for 10 weeks

Summary of Intended Learning Outcomes

-Students will be able to use the notation of CASL to formulate informally-described properties of functions and data types and to structure specifications into appropriate units.
-Students will be able to prove properties of functions and data types specified in CASL using induction and methods of equational reasoning, both by hand and using the CASL tool set.
-Students will be able to apply the notation of CASL architectural specifications to describe the modular structure of systems consisting of about a dozen modules, and to develop programs of about 100 lines from CASL specifications by modular decomposition and stepwise refinement.
-Students will be able to explain aspects of the theoretical underpinnings of CASL (algebras, homomorphisms, congruences etc.) and to prove simple properties involving these concepts.