CSC3332 : Programming Language Design and Verification (Inactive)
- Inactive for Year: 2019/20
- Module Leader(s): Dr Stephen Riddle
- Owning School: Computing
- Teaching Location: Newcastle City Campus
|Semester 1 Credit Value:||20|
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).
(Focusses on the "Structured Operational Semantics" technique.)
Covering large definitions (PL/I, Ada, Java) and different (to SOS) approaches
- 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
- prototype code generation of correct compiler
|Guided Independent Study||Assessment preparation and completion||1||1:30||1:30||Examination|
|Guided Independent Study||Assessment preparation and completion||21||0:30||10:30||Revision to end of semester exam and exam duration|
|Guided Independent Study||Assessment preparation and completion||22||1:00||22:00||Lecture follow-up|
|Scheduled Learning And Teaching Activities||Lecture||22||1:00||22:00||Traditional lectures|
|Scheduled Learning And Teaching Activities||Practical||22||2:00||44:00||Computer classroom|
|Guided Independent Study||Project work||1||25:00||25:00||Coursework|
|Guided Independent Study||Independent study||75||1:00||75:00||Background reading|
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.
The format of resits will be determined by the Board of Examiners
|Practical/lab report||1||M||50||3500 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%.