Undergraduate

modules

Modules

CSC3332 : Programming Language Design and Verification (Inactive)

Semesters
Semester 1 Credit Value: 20
ECTS Credits: 10.0

Aims

Programming languages come and go - if you make a career in computing, there is no doubt that you will have to learn languages which do not even exist today. This is in addition to literally thousands of general purpose languages, there are those tailored for specific applications like gaming, virtual reality, text layout, robotics, etc. Sadly, many languages embody one new idea (e.g. objects, concurrency, remote execution) but are significantly *worse* than their predecessors in other respects

The principal aim of this module is to communicate ways of understanding and documenting the key ideas in a language. The material should equip you to make sense of the many languages you will meet in your career. If you design new languages, they will benefit from you being able to manipulate the key concepts.

Furthermore, to make sure the complexities (and scale) of language design are addressed, you will also be trained in practical aspects of formal modelling and verification. For this we will use a well-founded approach following a set of mature formal tools and techniques within software engineering.

Outline Of Syllabus

Introduction - syntax versus semantics
Syntax - (concrete versus abstract; context conditions).
Semantics (meaning)
(Focusses on the "Structured Operational Semantics" technique.)
Revision/other approaches

Covering large definitions (PL/I, Ada, Java) and different (to SOS) approaches

Introduction
- nature of software verification principles (correctness, abstraction, refinement, design decisions, documented assumptions, model-based testing, etc.)
- understanding expertise required and costs involved; identifying the right technique to the task at hand.

Modelling and Specification
- key notions of functional programming: induction, recursion, termination, datatypes, type classes, referentially transparent, etc.
- basics notions of verification tools: Isabelle 101, structural induction, tooling for language design.
- elicitation and proof of properties of interest: compilation x interpretation agreement, language transformations, etc.
- improved language-design decisions: type system extensions (e.g. security-types, etc.), feature extension (e.g. OO + concurrency), etc.
- code-contracts and programming correctness reasoning
Prototyping:
- prototype code generation of correct compiler

Teaching Methods

Teaching Activities
Category Activity Number Length Student Hours Comment
Guided Independent StudyAssessment preparation and completion11:301:30Examination
Guided Independent StudyAssessment preparation and completion210:3010:30Revision to end of semester exam and exam duration
Guided Independent StudyAssessment preparation and completion221:0022:00Lecture follow-up
Scheduled Learning And Teaching ActivitiesLecture221:0022:00Traditional lectures
Scheduled Learning And Teaching ActivitiesPractical222:0044:00Computer classroom
Guided Independent StudyProject work125:0025:00Coursework
Guided Independent StudyIndependent study751:0075:00Background reading
Total200:00
Teaching Rationale And Relationship

Lectures are used to impart knowledge and practicals are used to provide experience of the solution of problems and understanding of decisions in practice.

Assessment Methods

The format of resits will be determined by the Board of Examiners

Exams
Description Length Semester When Set Percentage Comment
Written Examination901A50N/A
Other Assessment
Description Semester When Set Percentage Comment
Practical/lab report1M503500 words
Assessment Rationale And Relationship

The unseen examination will allow assessment of acquired knowledge using short bookwork questions, the ability to apply that knowledge using application questions, & time-constrained assessment of subject-specific skills using application questions.

The coursework will allow in-depth assessment of cognitive and subject-specific programming skills.

There is one system design and analysis assignment assessing the understanding of basic concepts of the modelling and analysis of concurrent systems through a simple case study using the Workcraft toolkit developed at Newcastle. The coursework will involve design of a model, its implementation as a Petri net, formulation of analytical requirements, and automatic checking of these requirements.

The examination is based around theoretical issues involved in a problem solving task. It is an "open book" examination paper, and nothing needs to be learnt by heart to pass it.

The purpose of the problem solving exercises is to familiarise the students with the software for modelling and verification of concurrent systems, and to practice the modelling techniques learnt at the lectures.

N.B. This module has both “Exam Assessment” and “Other Assessment” (e.g. coursework). If the total mark for either assessment falls below 35%, the maximum mark returned for the module will normally be 35%.

Reading Lists

Timetable