The unit introduces the formal study of software systems. It is intended to provide a general basis for further study or research in software-focused areas of Computer Science such as Programming Languages and Formal Methods.
The unit is organised around two main themes:
a) The meaning of programs. To study software systems it is necessary to have a proper understanding of the programming languages in which those systems are written. Formal semantic descriptions of languages assign mathematical meanings to programs. Typical kinds of meaning that will be studied include types that specify the operations that programs will perform, and operational aspects that capture how a program behaves as it executes.
b) Techniques for verifying that languages and programs have desired properties. We will see how to analyse a language semantics to prove that all programs written in that language have desirable properties. E.g., a desirable property of a type system is type safety: that an executing program cannot execute an illegal operation. We will also study the properties of particular programs. E.g., it is often desirable to be able to prove that a program produces a desired result.
The practical work in the unit will include implementation of formal language semantics and development of verification proofs. We emphasise the use of frameworks and tools to assist with both of these activities. Examples include the use of software language engineering tools and libraries to assist with language implementation, and the use of proof assistants, program verification systems or model checkers to help us specify properties and to find proofs.
Students entering this unit should have reasonable programming experience and should have studied discrete mathematics. Relevant Macquarie University units for programming maturity are COMP225 Algorithms and Data Structures, COMP229 Object-Oriented Programming Practices and any 300-level unit that applies programming skills to particular problem domains (e.g., COMP330 Computer Graphics, COMP333 Algorithm Theory and Design, and ISYS302 Advanced Application Development). DMTH137 Discrete Mathematics I and DMTH237 Discrete Mathematics II provide good mathematical background. Previous courses in areas such as programming language concepts or implementation, such as COMP332 Programming Languages, will be helpful, but are not required.
The class material will be structured according to the following schedule. The rightmost column refers to the relevant chapters of the "Software Foundations" required text. Note that there will be no class in Week 5 and Week 7 due to the Easter Monday and Anzac Day holidays, respectively.
||Chapter of Text
||Introduction, Functional Programming
||Proof by Induction, Structured Data
||Polymorphism and Higher-Order Functions
||More basic tactics
||Maps, Imperative Programming Language
||Hoare Logic for Imperative Programs
||Smallstep Operational Semantics
||Simply-Typed Lambda Calculus
||Stlc, StlcProp (overview)