This is the course website for:
ANU COMP1600/6260 Foundations of Computing S2 2024
| COMP1600/COMP6260 | |
|---|---|
| Mode of Delivery | on campus |
| Prerequisites | See programs and courses for COMP1600/COMP6260 |
| Lecture 1 | Monday, 2 pm to 3 pm, Llewellyn Hall, at the School of Music building (number 100) |
| Lecture 2 | Tuesday, 2 pm to 4 pm, same place |
| Course Convenors | Prof. Dirk Pattinson and Dr. Pascal Bercher |
Course overview
This course presents some formal notations that are commonly used for the description of computation and computing systems, for the specification of software, and for mathematically rigorous arguments about program properties. The first part of the course focuses on understanding programs in terms of assertions that can be verified using the Dafny Verifier. Dafny is a programming language that allows us to annotate programs and formally establish the validity of assertions, including proving basic properties expressed in logic. Weekly mini-assignments using Dafny will be part of the course, and students will need to submit Dafny code. The second part of the course covers formal language theory, particularly regular expressions, finite state machines, Turing Machines, and context-free grammars, as well as their induced languages languages.