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
Credit level (Normal year taken)SCQF Level 11 (Postgraduate) AvailabilityAvailable to all students
SCQF Credits10 ECTS Credits5
SummaryThe 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
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.
Information for Visiting Students
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).

Additional Information
Course URL
Graduate Attributes and Skills 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
Combined Course Timetable
Important Information
© Copyright 2014 The University of Edinburgh - 12 January 2015 4:11 am