Postgraduate Course: Theory and Practice of Algebraic Specifications (INFR11026)
Course Outline
| School | School of Informatics |
College | College of Science and Engineering |
| Credit level (Normal year taken) | SCQF Level 11 (Postgraduate) |
Availability | Available to all students |
| SCQF Credits | 10 |
ECTS Credits | 5 |
| Summary | 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.). |
| Course description |
* Motivation.
o Modelling systems as algebras, describing functional behaviour, formal software development.
* Theory.
o Universal algebra: signatures, algebras, homomorphisms, congruences, term algebras, term evaluation, signature morphisms, reducts.
o Simple equational specifications: satisfaction and the Satisfaction Lemma, flat specifications, Birkhoff Variety Theorem, theories, equational calculus, initial models, structural induction, term rewriting.
o Working within an arbitrary logical system: institutions, flat specifications in an arbitrary institution, institutions with extra structure.
o Structured specifications: specification-building operations and their semantics, how to roll your own, specification languages, the category of specifications, algebraic laws for structured specifications
o Further topics: parameterised specifications, parameterised programs, and specifications of parameterised programs; extending to higher-order; formal program development, stepwise development, modular decomposition; behavioural equivalence, behavioural abstraction, modular development and stability; proving theorems about modular specifications; the category of institutions, heterogeneous specifications.
* Practice.
o The Common Algebraic Specification Language (CASL). Basic specifications, subsorts, structured specifications, generic specifications, views, architectural specifications. Methodological issues.
o Using the CASL tool set.
Relevant QAA Computing Curriculum Sections: Programming Fundamentals, Software Engineering, Systems Analysis and Design, Theoretical Computing
|
Information for Visiting Students
| Pre-requisites | None |
Course Delivery Information
| Not being delivered |
Learning Outcomes
1 - 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.
2 - 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.
3 - 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.
4 - 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.
|
Reading List
* D. Sannella and A. Tarlecki. Essential concepts of algebraic specification and program development. Formal Aspects of Computing 9:229-269 (1997).
* Selected parts of the draft of the book: D. Sannella and A. Tarlecki. Foundations of Algebraic Specifications and Formal Program Development.
* M. Bidoit and P. Mosses. CASL User Manual. Springer LNCS 2900 (2004).
|
Contacts
| Course organiser | Dr Michael Rovatsos
Tel: (0131 6)51 3263
Email: mrovatso@inf.ed.ac.uk |
Course secretary | Miss Gillian Bell
Tel: (0131 6)50 2692
Email: Gillian.Bell@ed.ac.uk |
|
|
University Homepage