- ARCHIVE for reference only

University Homepage
DRPS Homepage
DRPS Search
DRPS Contact
DRPS : Course Catalogue : School of Informatics : Informatics

Postgraduate Course: Theory and Practice of Algebraic Specifications (INFR11026)

Course Outline
SchoolSchool of Informatics CollegeCollege of Science and Engineering
Course typeStandard AvailabilityAvailable to all students
Credit level (Normal year taken)SCQF Level 11 (Postgraduate) Credits10
Home subject areaInformatics Other subject areaNone
Course website Taught in Gaelic?No
Course descriptionThe 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 (not applicable to Visiting Students)
Pre-requisites Co-requisites It is RECOMMENDED that students also take Functional Programming and Specification (Level 10) (INFR10043) OR Functional Programming and Specification (Level 9) (INFR09033)
Prohibited Combinations Other requirements For Informatics PG students and final year MInf students only, or by special permission of the School.
Additional Costs None
Information for Visiting Students
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

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
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
KeywordsNot entered
Course organiserDr Michael Rovatsos
Tel: (0131 6)51 3263
Course secretaryMiss Gillian Bell
Tel: (0131 6)50 2692
Help & Information
Search DPTs and Courses
Degree Programmes
Browse DPTs
Humanities and Social Science
Science and Engineering
Medicine and Veterinary Medicine
Other Information
Important Information
© Copyright 2011 The University of Edinburgh - 16 January 2012 6:17 am