This module will cover predicate logic and set theory, which will provide a basic tool-kit for formal descriptions in computer science.

The topics covered will include:

• Propositional logic, syllogistic reasoning and predicate logic
• Basic definitions in set theory, including relations, functions etc.
• Theorem proving using natural deduction

As well as proving a basis for formal descriptions, logic is used in software engineering (e.g. OCL, design-by-contract, Spec#), logic-based techniques are important in program analysis (e.g. pointer analysis, object ownership), and logics can be used to formulate advanced type systems for programming languages (polymorphism, generics and higher-order types). One of the most important logical problems, the Entscheidungsproblem was a key motivation in the foundation of computer science in the 1930s.

The textbook is

• Logic in Action by Johan van Benthem, Hans van Ditmarsch, Jan van Eijck, Jan Jaspars, available from logicinaction.org, 2014.

See also: university module description

The aim of this module is to explore the relationship between uncertainty, logic and computation. Traditionally, logic and computation have focused on the deduction of certain knowledge, neglecting the role of uncertainty and its computational manifestation. One component of the module will focus on epistemic modal logic, which extends formal classical logics to express reasoning about knowledge and information. Another component will consider the computational nature of reliability and its role in defining standards of measurement and systems of representation. Concepts such as the measurement problem, the private language argument, logical depth and the connection between data compression, prediction and understanding will be explored, with a focus on how finite objects can be used to reliably communicate Platonic ideals.

• Formalize and evaluate the validity of statements in modal logic
• Explain the relationship between data compression, prediction and understanding
• Discuss the limitations of non-computational models of uncertainty and probability
• Elucidate the computational foundations of standards of measurement
• Debate how finite objects can be used to reliably communicate Platonic concepts

See also: university module description

This module explores the foundation of Computer Science, laid with the discovery of (computationally) unsolvable problems in the 1930s.

A particular feature of the module is its focus on reading primary sources from the period, starting with Gödel's 1931 incompleteness theorem and moving on through the results of Church, Turing and Post in 1936. Here, "primary sources" are taken as being the published research work of scientists, in their full and original form (or in translation). The central idea is to bypass all interpretations, simplifications and explanations, and put you in direct contact with the words of these pioneers, as one scientist to another.

The historical and scientific background, from Frege and Russell through Hilbert's programme is also reviewed. In this context, computer science can be seen as part of a tradition of human enquiry spanning many generations, rather than just a collection of technological novelties. This module lays a solid basis for considering future developments in the foundations of computer science.

The papers we'll be covering are:

• Kurt Gödel, "On formally undecidable propositions of Principia Mathematica and related systems", Monatshefte für Mathematik und Physik 38 (1931), pp 173-198.
• Alonzo Church, "An unsolvable problem of elementary number theory", American Journal of Mathematics, 58 (1936), pp 345-363.
• Alan M. Turing, "On Computable Numbers, with an Application to the Entscheidungsproblem", Proceedings of the London Mathematical Society, 2 42 (1937) pp 230-65.
• Emil L. Post, "Recursively enumerable sets of positive integers and their decision problems", Bull. Amer. Math. Soc. 50(5) (1944), 284-316.

General Reading

This module is fairly theoretical in content, and will be based closely on the above papers. Some text related to these papers include:

• The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, Martin Davis, Dover 2004.
  Contains the text of these papers and some others from the period - just the papers and a brief introduction, no discussion.
• The Annotated Turing, Charles Petzold
  An in-depth study of Turing's paper with lots of background material.
• Gödel's Theorem: An Incomplete Guide to Its Use and Abuse, Torkel Franzén, CRC Press, 2005.
  A serious review of Godel's theorems and a discussion of how they should (and shouldn't) be used.
• An Introduction to Gödel's Theorems, Peter Smith, Cambridge University Press, 2013.
  Apparently aimed at philosophy students, but still provides a very comprehensive background to the theorems.

• Logicomix: An Epic Search for Truth by Apostolos Doxiadis and Christos Papadimitriou
• The Universal Computer: The Road from Leibniz to Turing by Martin Davis
• Gödel, Escher, Bach: An Eternal Golden Braid by Douglas Hofstadter

See also: university module description

• Develop a fuller understanding of what exactly these techniques are analysing, and why
• Understand the limitations of program analysis: what can and can't be determined by looking at programs
• Deepen our understanding of how programs actually work - what happens ``under the hood''

• refactor, re-engineer or reclaim existing software
• reverse-engineer a class diagram from some source code
• examine source code to see if it adheres to particular coding guidelines
• apply software metrics to code, to measure its design quality
• instrument the code, for example, to measure statement or branch coverage during testing
• transform the code into a different format (e.g. to another programming language)
• ..... and many others

Background Reading

To get a flavour of what this modules is about, have a look through chapters 9 and 12 of Compilers: Principles, Techniques and Tools (Second Edition) by Alfred V. Aho, Monica S. Lam, Ravi Sethi, Jeffrey D. Ullman, Addison Wesley, 2007. ISBN: 978-0321491695.

Another approach would be to have a look through some relevant conference proceedings: we'll be reading through some of these in the module. Some of the more relevant conferences include:

• International Conference/Workshop on Program Comprehension
• Working Conference on Reverse Engineering
• Working Conference on Source Code Analysis and Manipulation

This module is currently scheduled to take place in semester 2. If you've any queries about the module in advance of this, please don't hesitate to contact me.

The software engineering toolsmith

CS619 is designed to give you the basic skills needed to develop your own tools that you can then use to build better software. Relatively few craftsmen get to use their skills to build their own tools and shape them to their own particular requirements...

See also: university module description