# Yearbooks 2016 2017 2018 2020 2021

## 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 Programmes 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

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 each student to familiarise himself or herself 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.