Formal aspects of computing (I) 740

Modulekode COS 740
Kwalifikasie Postgraduate
Fakulteit Faculty of Engineering, Built Environment and Information Technology

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.

Modulekrediete 15.00
NQF Level 08
Prerequisites No prerequisites.
Contact time 2 lectures per week
Language of tuition Module is presented in English
Department Computer Science
Period of presentation Semester 1 or Semester 2

Die inligting wat hier verskyn, is onderhewig aan verandering en kan na die publikasie van hierdie inligting gewysig word.. Die Algemene Regulasies (G Regulasies) is op alle fakulteite van die Universiteit van Pretoria van toepassing. Dit word vereis dat elke student volkome vertroud met hierdie regulasies sowel as met die inligting vervat in die Algemene Reëls sal wees. Onkunde betrefffende hierdie regulasies en reels sal nie as ‘n verskoning by oortreding daarvan aangebied kan word nie.

Copyright © University of Pretoria 2023. All rights reserved.

COVID-19 Corona Virus South African Resource Portal

To contact the University during the COVID-19 lockdown, please send an email to [email protected]

FAQ's Email Us Virtual Campus Share Cookie Preferences