Yearbooks

Formal aspects of computing (I) 740


 
Module code COS 740
Qualification Postgraduate
Faculty Faculty of Engineering, Built Environment and Information Technology
Module content

The focus of this module is on a formal approach to deriving algorithms, known as “correctness by construction”. It relies on Dijkstra's guarded command language (GCL) for specifying the derived algorithms. The requirements of an algorithm are initially stated in terms of a pre- and a post-condition, specified in first order predicate logic. Strategies are given for progressively refining these specifications to GCL notation which can, in turn, easily be translated into a conventional programming language. The surprising power of the method will be demonstrated. Not only are algorithms guaranteed to be correct (in the same sense that the proof of a mathematical theorem is guaranteed to be correct); they frequently turn out to be remarkably efficient. In the early part of the module, a number of well-known algorithms (such as linear and binary search, raising a number to an integer power, finding the approximate log of a number, etc) will be derived in order to become thoroughly familiar with the approach. Later various intermediate level algorithms will be derived (such as simple raster drawing algorithms, pattern matching algorithms, finding the longest string of a certain type, an algorithm to solve the majority voting problem, etc). Finally, the method will be used to derive state-of-the-art algorithms to minimize finite automata and to construct formal concept lattices. The theory necessary to understand these topics will be provided. The value-objectives of the module are: to develop an appreciation that theory can be effectively deployed to solve practical problems; to value the elegance of the algorithmic solutions; and to value a correctness-by-construction mindset over one that is content with debugging into correctness. A basic understanding is assumed of first order predicate logic, as well as competency in mathematical reasoning.

Module credits 15.00
Prerequisites No prerequisites.
Contact time 2 lectures per week
Language of tuition Module is presented in English
Academic organisation Computer Science
Period of presentation Semester 1 or Semester 2

The information published here is subject to change and may be amended after the publication of this information. The General Regulations (G Regulations) apply to all faculties of the University of Pretoria. It is expected of students to familiarise themselves well with these regulations as well as with the information contained in the General Rules section. Ignorance concerning these regulations and rules will not be accepted as an excuse for any transgression.

Copyright © University of Pretoria 2024. All rights reserved.

FAQ's Email Us Virtual Campus Share Cookie Preferences