How to define the formal and informal semantics of an algorithm as accurately as possible?

Question

I am currently researching ways to define the semantics of programs for some ideas I have for a new programming language. Most ways to define semantics involve mapping the programming language syntax representation of a program to some semantic specification. I dislike this approach, because the syntax restricts what semantics you are able to express and it often results in the under and over specification of the semantics.

Instead of thinking of a programming language in terms of syntax constructs and their corresponding semantics, I want to focus on semantics first, syntax, although important to be able to best read and write programs and ultimately necessary to formulate the semantics, is of lesser importance. But in order to do so, I need a language that is capable of defining the semantics as accurately as possible. This semantic language should not be a programming language by itself, because its main purpose is defining semantics accurately, not computations. So I think most formal semantic specifications do not comply to these requirements, because they focus on extracting semantics out of existing programs instead of defining them as accurately as possible in the first place. Therefore I would like to ask the following question:

"Are there any languages or methods that focus mainly on expressing formal and informal semantics of an algorithm as accurately as possible?"

During my research I was reading "Formal Syntax and Semantics of Programming Languages" by Kenneth Slonneger which include some chapters about the different ways to define the semantics for a programming language. In chapter 11 (Axiomatic Semantics), page 397, he states that "Extensive literature has dealt with the difficult problem of accurate specifications of algorithms.". But I have a difficult time finding literature that is specific about "accurate specifications of algorithms". Therefore my second question is as follows:

"Do you know about any literature that specificly talks about how to define accurate specifications of algorithms?"

Edit: To make more clear what I mean by "expressing semantics of an algorithm as accurately as possible" I will give an example. If with axiomatic semantics the following pre and post conditions were given:

pre  = m >= 0 and n >= 0
post = minimum <= m and minimum <= n and minimum >= 0

Then the following function would comply:

minimum m n = 0

But this does not capture the intent the person writing the specification had.

"Do you know of methods that could capture this intent more accurately?"

Answer 1

I cannot tell from your question how deep your understanding of syntax and semantics is, but I see some pitfalls there. A programming language has an indispensable syntactic component. It also has a semantic component. And there is the connection between syntax and semantics.

There are many semantic structures that have been proposed to give meaning to programming languages. These vary from operational semantics to domain theoretic structures. If you want to start with semantics, you can identify a space of domains and then try to define a language that can express properties of these domains. Samson Abramsky, in his PhD thesis, showed that this process can be made very systematic.

Domain Theory in Logical Form, Samson Abramsky, PhD Thesis, 1987.

Specifically, this dissertation shows that there is a family of semantic structures, a family of logics, a family of topological spaces, and a programming language that sit in very tight correspondence (think isomorphism). You can start with one family of objects and derive the other. Samson's work allows you to start with semantic structures and derive a logic, for example.

Answer 2

I don't know how you can define the informal semantics as accurately as possibly, but there does exist machinery for defining semantics that is purely, well, semantic.

Your semantics could be based on mathematical functions, relations, or domains. Indeed, the style of semantics known as Denotational Semantics builds upon these (and other) semantic notions by mapping the syntax in a compositional fashion to some semantic domain.

If you don't want syntax for your programming language, then start directly with the semantic domains (for example, those from Domain Theory). In this setting, each type in your programming language will be represented by a semantic domain and algorithms will then be functions from one type to another.

Answer 3

There are unfortunate confusions in the way you have posed the question.

Programs have semantics. Programming Languages are given semantic definitions. In more detail: every program has a meaning, either as a computation or as a mathematical function (relation, trace set, strategy,...). A semantic definition is given for an entire programming language, so that the meaning of every program in the language is defined.

Programs can also be given specifications. While the semantics of the program says what the program means, its specification states what we care about its behaviour. So, the specification can be partial. It need not state what the program does under all possible situations. Neither does it need to state everything about the outputs of the program, only the properties we care about.

The sample specification you have shown for the minimum function is incomplete. It says that the output has to be smaller than (or equal to) both its inputs, but it does not say that the output must be one of the two inputs. To make it complete (which is apparently the "intent"), you need to add this condition

minimum = a or minimum = b

To read about the various techniques used for specifying programs, you might read books like:

• David Gries, Science of Programming
• John Reynolds, Craft of Programming

If you are interested in functional programs rather than imperative programs, then a good starting point is

• Bird and Wadler, Functional Programming

For a quick starting point, you might read the lecture Handout on "Specification and Verification of Functional Programs" of my Lecture Notes on Principles of Programming Languages.