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

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?"

• This question is too broad. It has two possible answers. The first possible answer is "yes". The other one is a survey paper, and you've already found a book. So how do you want us to answer? Also, it would help if you tell us a bit about your background. Did you just randomly walk into the area of programming semantics, or have you done some work in it before? Dec 6, 2012 at 4:23
• I have edited my question, hopefully it made it less broad. Yes, I am new to the area of programming semantics, but after reading several books and papers I have yet to find the answer I am looking for. How to best capture intent? But I am afraid it is a bit to philosophical in nature. Because how does one capture meaning in a conceptual world? But I am already happy if I learn of a way to describe a good enough approximation of the intended meaning, so I can capture most of the semantic bugs in my programming language. Dec 7, 2012 at 12:00

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.

• Excellent concrete starting point. Dec 10, 2012 at 23:27
• Abramsky's thesis might be a bit too technical for the needs of this questioner. Mar 8, 2013 at 9:09
• @UdayReddy, I agree. I still discover new and interesting material I haven't appreciated every time I look at that thesis. I went for a complicated answer because I don't know enough to provide a simple answer. Mar 9, 2013 at 20:17

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.

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