Durham University
Programme and Module Handbook

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