Postgraduate Course: Theory and Practice of Algebraic Specifications (INFR11026)
Course Outline
| School | School of Informatics |
College | College of Science and Engineering |
| Course type | Standard |
Availability | Available to all students |
| Credit level (Normal year taken) | SCQF Level 11 (Postgraduate) |
Credits | 10 |
| Home subject area | Informatics |
Other subject area | None |
| Course website |
http://www.inf.ed.ac.uk/teaching/courses/tpas |
Taught in Gaelic? | No |
| Course description | 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.). |
Information for Visiting Students
| Pre-requisites | None |
| Displayed in Visiting Students Prospectus? | Yes |
Course Delivery Information
| Not being delivered |
Summary of Intended 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. |
Assessment Information
Written Examination 70
Assessed Assignments 30
Oral Presentations 0
Assessment
Two written exercises, equally weighted -- one on the practical strand, and one on the theory strand.
If delivered in semester 1, this course will have an option for semester 1 only visiting undergraduate students, providing assessment prior to the end of the calendar year. |
Special Arrangements
| None |
Additional Information
| Academic description |
Not entered |
| Syllabus |
* 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 |
| Transferable skills |
Not entered |
| 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).
|
| Study Abroad |
Not entered |
| Study Pattern |
Not entered |
| Keywords | Not entered |
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