Undergraduate Programme and Module Handbook 2007-2008 (archived)
Module COMP2171: PROGRAMMING AND REASONING
Department: Computer Science
COMP2171: PROGRAMMING AND REASONING
| Type | Open | Level | 2 | Credits | 20 | Availability | Available in 2007/08 | 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