Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

What is "formal semantics"?

I'm reading a very silly paper and it keeps on talking about how Giotto defines a "formal semantics".

Giotto has a formal semantics that specifies the meaning of mode switches, of intertask communication, and of communication with the program environment.

I'm on the edge of, but just cannot quite grasp what it means by "formal semantics."

like image 338
bobobobo Avatar asked Feb 28 '10 23:02

bobobobo


People also ask

What is the example of formal semantics?

For instance, to know the meaning of the English sentence "Nancy smokes" one has to know that it is true when the person Nancy performs the action of smoking. However, many current approaches to formal semantics posit that there is more to meaning than truth-conditions.

What is the point of formal semantics?

Formal semantics of a programming language give a rigorous mathematical description of the meaning of this language, to enable a precise and deep understanding of the essence of the language beneath its syntax.

What are the 3 kinds of semantics?

Semantics Meanings: Formal, Lexical, and Conceptual Semantic meaning can be studied at several different levels within linguistics. The three major types of semantics are formal, lexical, and conceptual semantics.

What are the two types of semantics?

Semantics is the study of meaning. There are two types of meaning: conceptual meaning and associative meaning.


3 Answers

To expand on Michael Madsen's answer a little, an example might be the behaviour of the ++ operator. Informally, we describe the operator using plain English. For instance:

If x is a variable of type int, ++x causes x to be incremented by one.

(I'm assuming no integer overflows, and that ++x doesn't return anything)

In a formal semantics (and I'm going to use operational semantics), we'd have a bit of work to do. Firstly, we need to define a notion of types. In this case, I'm going to assume that all variables are of type int. In this simple language, the current state of the program can be described by a store, which is a mapping from variables to values. For instance, at some point in the program, x might be equal to 42, while y is equal to -5351. The store can be used as a function -- so, for instance, if the store s has the variable x with the value 42, then s(x) = 42.

Also included in the current state of the program is the remaining statements of the program we have to execute. We can bundle this up as <C, s>, where C is the remaining program, and s is the store.

So, if we have the state <++x, {x -> 42, y -> -5351}>, this is informally a state where the only remaining command to execute is ++x, the variable x has value 42, and the variable y has value -5351.

We can then define transitions from one state of the program to another -- we describe what happens when we take the next step in the program. So, for ++, we could define the following semantics:

<++x, s> --> <skip, s{x -> (s(x) + 1)>

Somewhat informally, by executing ++x, the next command is skip, which has no effect, and the variables in the store are unchanged, except for x, which now has the value that it originally had plus one. There's still some work to be done, such as defining the notation I used for updating the store (which I've not done to stop this answer getting even longer!). So, a specific instance of the general rule might be:

<++x, {x -> 42, y -> -5351}> --> <skip, {x -> 43, y -> -5351}>

Hopefully that gives you the idea. Note that this is just one example of formal semantics -- along with operational semantics, there's axiomatic semantics (which often uses Hoare logic) and denotational semantics, and probably plenty more that I'm not familiar with.

As I mentioned in a comment to another answer, an advantage of formal semantics is that you can use them to prove certain properties of your program, for instance that it terminates. As well as showing your program doesn't exhibit bad behaviour (such as non-termination), you can also prove that your program behaves as required by proving your program matches a given specification. Having said that, I've never found the idea of specifying and verifying a program all that convincing, since I've found the specification usually just being the program rewritten in logic, and so the specification is just as likely to be buggy.

like image 192
Michael Williamson Avatar answered Nov 05 '22 16:11

Michael Williamson


Formal semantics describe semantics in - well, a formal way - using notation which expresses the meaning of things in an unambiguous way.

It is the opposite of informal semantics, which is essentially just describing everything in plain English. This may be easier to read and understand, but it creates the potential for misinterpretation, which could lead to bugs because someone didn't read a paragraph the way you intended them to read it.

A programming language can have both formal and informal semantics - the informal semantics would then serve as a "plain-text" explanation of the formal semantics, and the formal semantics would be the place to look if you're not sure what the informal explanation really means.

like image 10
Michael Madsen Avatar answered Nov 05 '22 17:11

Michael Madsen


Just like the syntax of a language can be described by a formal grammar (e.g. BNF), it's possible to use different kinds of formalisms to map that syntax to mathematical objects (i.e. the meaning of the syntax).

This page from A Practical Introduction to Denotational Semantics is a nice introduction to how [denotational] semantics relates to syntax. The beginning of the book also gives a brief history of other, non-denotational approaches to formal semantics (although the wikipedia link Michael gave goes into even more detail, and is probably more up-to-date).

From the author's site:

Models for semantics have not caught-on to the same extent that BNF and its descendants have in syntax. This may be because semantics does seem to be just plain harder than syntax. The most successful system is denotational semantics which describes all the features found in imperative programming languages and has a sound mathematical basis. (There is still active research in type systems and parallel programming.) Many denotational definitions can be executed as interpreters or translated into "compilers" but this has not yet led to generators of efficient compilers which may be another reason that denotational semantics is less popular than BNF.

like image 3
datageist Avatar answered Nov 05 '22 16:11

datageist