The LEGO Project

The LEGO Project is a group of researchers interested in using the computer to help in developing and checking proofs. This page gives a brief overview of the project.

As software takes on a greater role in modern society, its reliability becomes a matter of increasing concern. There are many aspects to producing reliable software, including requirements analysis and specification. Our project focuses on computer-aided formal reasoning: using the computer to help in developing and checking proofs, in particular proofs of program correctness.

One of our long-term aims is to enable more people to feel confident about carrying out mathematical proofs, by providing them with computer assistance. There is a difference between proofs done with pencil and paper using ``mathematical English'' and formal proofs in logical notation developed on a computer. This is like the distinction between the informal description of an algorithm and its implementation as a program in a particular language. We have adapted technology used in software development, including tools such as parsers, type-checkers and interpreters, to help us in formal proof development.

Theoretical results justify our confidence in our proof environment. The project uses a constructive type theory as the primary framework for proofs. Constructive type theories can be regarded as hybrids between on the one hand the logic and set theory that mathematics is usually based on, and on the other hand functional programming languages with types. Constructive type theories are useful for reasoning about not only functional programs, but also programs written in idealised versions of widely-used languages such as C and Fortran. A particularly useful feature of modern type theories is their support for inductive definitions. Such definitions are commonly encountered in computer science, for example in defining mathematical models of programming languages.

Randy Pollack developed the system called LEGO, which we use extensively and continue to develop. LEGO supports:

• interactive proof construction,
• proof checking as type-checking,
• modular support for proof re-use, and libraries of definitions and theorems.

Helping programmers get it right

Programming errors can be avoided if the software engineer proves that his program fulfils the desired specification. This is difficult because programs are complex mathematical objects.

What is a good theory for developing programs and their correctness proofs? We are exploring type theory as a framework for program development methodologies which simultaneously support proving correctness properties.

LEGO's type theory provides

• a programming language dealing with expressions,
• inductive definitions naturally representing the syntax of a programming language. They are also crucial in modelling program execution on an abstract machine, and
• a logic which gives rise to a powerful specification language.

Combining all these features, we can cater for various notions of ``program correctness''. We analyse collections of refinement rules to guide the programmer. The LEGO system provides excellent support for proving that the rules cannot lead to ill-behaved programs (soundness) and that the collection of rules is sufficient regardless of the task at hand (completeness). Furthermore, the framework can be evaluated by case studies of program developments within LEGO.

We are investigating developing object-oriented programs together with their proofs of correctness, in collaboration with the Universities of Darmstadt and Erlangen.

Ongoing activities of the group include:

• co-operating with Harlequin Ltd. in studying the specifications and correctness proofs for memory management systems,
• creating a framework for developing imperative programs together with proofs of correctness,
• studying basic properties of constructive type theories and devising ways of improving the theories, and
• experimenting with other proof systems, with a view to simplifying the development and presentation of proofs on the computer.

• Drawing a straight line

  Computers do simple tasks quickly and reliably. Complex tasks have to be broken down into simple tasks. Even drawing a straight line on the screen is a complex task which must be broken down into simple instructions, telling the computer to paint some dots (picture elements, or pixels) on the screen. We describe two ways of drawing a line, two algorithms.

  ---

  Pixels

  If you look closely at the screen, you'll see that it is made up of a grid of small dots, called pixels (picture elements). There are about half a million pixels on a typical screen. The computer must be told what colour to use for each pixel, to create each image you see.

  Some images, such as photos, are stored as gif (Graphics Interchange Format) files, which store the colour of each pixel in the image. For images that can be represented as line drawings, it takes much less space to store a list of lines, and then compute which pixels should be coloured in each time we want to display the image. Drawing lines is the subject of this note.

  The pixels in a picture are arranged in rows and columns. We number the columns from left to right, starting with column zero at the left edge of the picture, and the rows from top to bottom, starting from zero at the top of the picture. So any pixel is described by two numbers, x,y, telling us where in the picture the pixel lies; x giving the column, and y giving the row.

  We call the pair of numbers, x,y, the coordinates of the pixel. In the demonstration applet below, we give a view magnified 10x, so a single pixel is represent by 100 actual pixels on the screen. Click on the yellow, diagram area of the applet below; the coordinates of the pixel you click on should appear in the message area.

  Lines

  A line can be described by giving two pixels, saying where the line should start and end. When you click on the diagram, a magnified point is drawn. When you click again, on another point, a line is drawn between the two points. How do we decide which pixels to draw to form the line? We describe two ways: recursive subdivision, and Bresenham's algorithm. You can see both in action by using the buttons to choose an algorithm, and then clicking in the yellow area to select the two ends of the line.