Undergraduate Programme and Module Handbook 2006-2007 (archived)

Module COMP2171: PROGRAMMING AND REASONING

Department: COMPUTER SCIENCE

COMP2171: PROGRAMMING AND REASONING

Type	Open	Level	2	Credits	20	Availability	Available in 2006/07	Module Cap	None.	Location	Durham

Prerequisites

Formal Aspects of Computer Science (COMP1021) AND EITHER Programming and Data Structures (COMP1082) OR Introduction to Programming (COMP1011).

Corequisites

None.

Excluded Combination of Modules

None.

Aims

To introduce the student to several new ideas in programming language design, and look at techniques used to study and verify the behaviour of programs.
The Declarative Programming sub-module will approach programming from a very different direction from Java, one that places emphasis on "what" we want a program to do rather than on precisely "how" it should be done, which results in a powerful framework for complex programming.
The specification and verfication will focus on various forms of semantics for programs and consider how we can reason about behaviour and implementation.
it is a significant application of the logic covered earlier in the course.

Content

Elementary programming techniques in a declarative language.
Advanced features of the language.
Type systems.
Modern programming language technologies.
Case studies.
Real-world programming.
Program semantics (e.g. operational semantics and axiomatic semantics such as weakest preconditions).
Techniques for program specification and verification.
Program logics such as Hoare logic and the associated specification and verification methods.
Application of logical semantics in analysis of programs.

Learning Outcomes

Subject-specific Knowledge:

To have an in-depth knowledge of programming through applying advanced concepts in programming languages and related methodologies and logic.
To demonstrate knowledge of the characteristics of declarative languages, their strengths and weaknesses for software production, and to be able to use them for simple problem solving.
To have surveyed a range of techniques concerning program semantics, program specification and verification, and to be able to apply these ideas to programs.

Subject-specific Skills:

Key Skills:

Modes of Teaching, Learning and Assessment and how these contribute to the learning outcomes of the module

Lecturing demonstrates what is required to be learned and the application of the theory to practical examples.
Problem classes through practicals provide assessment (both formative and summative) to guide students in the correct development of their knowledge and skills.
Tutorials provide active engagement and feedback to the learning process.
The end of year examinations assess the knowledge acquired and the ability to use this knowledge to solve problems.

Teaching Methods and Learning Hours

Activity	Number	Frequency	Duration	Total/Hours
Lectures	38	2 per week	1 hour	38
Tutorials	2		1 hour	2
Practicals	19	1 per week	2 hours	38
Preparation and Reading				122
Total				200

Summative Assessment

Component: Coursework		Component Weighting: 34%
Element	Length / duration	Element Weighting	Resit Opportunity
Coursework		100%
Component: Examination		Component Weighting: 66%
Element	Length / duration	Element Weighting	Resit Opportunity
two-hour examination		100%

Formative Assessment:

Example exercises given through the course.

■ Attendance at all activities marked with this symbol will be monitored. Students who fail to attend these activities, or to complete the summative or formative assessment specified above, will be subject to the procedures defined in the University's General Regulation V, and may be required to leave the University