Skip to navigation | Skip to main content | Skip to footer
Menu
Menu

COMP10112: Reasoning about Programs (2007-2008)

This is an archived syllabus from 2007-2008

Reasoning about Programs
Level: 1
Credit rating: 10
Pre-requisites: COMP10020
Co-requisites: an imperative language e.g. COMP10081
Duration: 11 weeks in second semester
Lectures: 14 in total, 2 per week
Examples classes: 4 in total, 1 per fortnight
Labs: 8 hours in total, 4 2-hr sessions
Lecturers: Kung-Kiu Lau
Course lecturer: Kung-Kiu Lau

Additional staff: view all staff
Timetable
SemesterEventLocationDayTimeGroup
Sem 2 w19-25,29-32 Lecture 3rdLab Fri 14:00 - 17:00 -
Assessment Breakdown
Exam: 60%
Coursework: 10%
Lab: 30%

Aims

The aim of this module is to introduce students to the principles and practice of reasoning about simple imperative programs. The principles will be based on first-order logic, and the practice will be provided by the imperative language SPARK and its tools

Learning Outcomes

Students should have a basic knowledge of first-order logic and should be able to understand sentences in first-order logic. (A)
Students should be able to write sentences in first-order logic and translate them to and from English sentences. (B)
Students should be able to understand first-order logic specification of simple properties of imperative programs. (A)
Students should be able to reason informally about simple imperative program properties specified in first-order logic. (B)
Students should be able to reason about SPARK programs. (B)
Students should be able to use Tarski's world in the lab to create universes and reason about them in first-order logic. (C)
Students should be able to use SPARK tools in the lab to write SPARK programs and reason about them. (C)
Students should be able to work to deadlines. (D)

Assessment of Learning outcomes

Learning outcomes (1), (2), (3) (4) and (5) are assessed by examination, learning outcomes (6) and (7) and (8) in the laboratory.

Contribution to Programme Learning Outcomes

A1, A5, B1, C6, D5

Syllabus

Introduction


Introductory Example [1]

Proving versus Testing [1]

Introduction to First-order Logic [2]

Reasoning about Imperative Programs (Part 1: Principles)



Pre-post-condition Specifications [1]

Commands as Predicate Transformers [4]

Assignments

Sequential Composition

Conditional Commands

Iterative Commands

Weakest Pre-Conditions

Reasoning about Imperative Programs (Part 2: Practice)


SPARK: An Introduction [1]

The SPARK Tools [1]

Path Functions [1]

Verification Conditions [1]

Using SPARK Tools in the Lab [1]

Reading List

The books mentioned in the COMP10021 syllabus will also be useful here.

There are many books on logic. One book that introduces logic to a wide readership using the Tarski's World software package will be used in the lab for this course.

Title: High Integrity Software: The SPARK Approach to Safety and Security
Author: John Barnes
ISBN: 0321136160
Publisher: Addison Wesley
Edition:
Year: 2003


Title: Language of First-Order Logic
Author: Jon Barwise, John Etchemendy
ISBN: 0937073997
Publisher: Center for the Study of Language and Information
Edition: 3rd Rev
Year: 1993