Mathematical Structures in Computer Science

Paper

Semantical proofs of correctness for programs performing non-deterministic tests on real numbers

THOMAS ANBERRÉEa1

a1 Division of Computer Science, University of Nottingham in Ningbo, China, 199 Taikang Road East, 315100, Ningbo, China Email: thomas.anberree@nottingham.edu.cn

Abstract

We consider a functional language that performs non-deterministic tests on real numbers and define a denotational semantics for that language based on Smyth powerdomains. The semantics is only an approximate one because the denotation of a program for a real number may not be precise enough to tell which real number the program computes. However, for many first-order total functions f : n, there exists a program for f whose denotation is precise enough to show that the program indeed computes the function f. In practice, it is not difficult to find programs like this that possess a faithful denotation. We provide a few examples of such programs and the corresponding proofs of correctness.

(Received May 06 2008)

(Revised December 09 2009)