I have a language for sensor networks (generates C code) and I want to define the formal semantics of it.

The language has this form:

{STATE name_state:
EVERY time
SELECT {variable [, variable] ...}
[SENDIF send_condition]
[CHANGEIF change_condition GOTO new_state];
} ...

START IN initial_state;
  • The initial state of the program is specified by the START IN instruction.
  • Each state is defined by the STATE instruction.
  • In the specification of each state the clauses EVERY and SELECT are compulsory and the clauses SENDIF and CHANGEIF are optional.
  • The CHANGEIF clause is only not specified when there is a single state.

What type of formal semantics is more convenient to use?

  • $\begingroup$ Are you after the formal semantics or a more formal way of describing the syntax? It sounds like the latter. $\endgroup$ – Dave Clarke Feb 18 '13 at 21:40
  • 1
    $\begingroup$ See his comment to my answer, looks like he's interested in both. $\endgroup$ – Yuval Filmus Feb 18 '13 at 23:58
  • $\begingroup$ Yuval Filmus, Dave Clarke I will describe the sintax using the Backus-Naur form and edit the question. $\endgroup$ – Claudio Biale Feb 19 '13 at 0:46
  • 1
    $\begingroup$ Perhaps some sort of timed automaton model. $\endgroup$ – Dave Clarke Feb 19 '13 at 11:16
  • 1
    $\begingroup$ Sounds suitable, from what information I have seen. $\endgroup$ – Dave Clarke Feb 21 '13 at 14:34

In general, axiomatic semantics is the nicest form of semantics, but is difficult to obtain for anything but the most simple languages, and subject of much current research. Denotational semantics is a vague term, if you mean domain theoretic semantics, then I advise against it. In general using operational semantics is easy and natural, especially if you use state-based SOS (structural operational semantics). The fact that you already have a translation into C is a strong indication that this would work in your case, because C can be seen as a state-based formalism.

Indeed your translation into C is a formal semantics of your sensor network language, albeit a painfully detailed one. So I guess you want a formal description that isto omit some level of detail (e.g. integers are 'real' mathematical integers and not some kind of finite modulo arithmetic). For this state-based SOS tends to be ideal.

  • $\begingroup$ You think I should work in the specified sensor network language? or feel that I have to work more at the generated code in C?. $\endgroup$ – Claudio Biale Feb 21 '13 at 13:09
  • 1
    $\begingroup$ @ClaudioBiale it depends on you and what you are trying to achieve. If you want to communicate with other people, then using C might not be helpful since few people voluntarily read code. A more abstract, less detailed presentation could be easier to understand. If you are just trying to clarify matters for yourself, writing an additional semantic account to accompany C code could be overkill. So there's no one answer to your question. $\endgroup$ – Martin Berger Feb 21 '13 at 13:27
  • $\begingroup$ Thanks for your reply. I want to formalize the semantics of the sensor network language. I'll look previous work using structured operational semantics and try to apply it in this language. $\endgroup$ – Claudio Biale Feb 21 '13 at 13:48
  • 1
    $\begingroup$ @ClaudioBiale That sounds like a good approach. $\endgroup$ – Martin Berger Feb 21 '13 at 14:50

Backus-Naur form used to be popular for these purposes. Another possibility is Wirth syntax notation. You can find other possibilities in the "see also" section of the article on Backus-Naur form.

  • 1
    $\begingroup$ Using the Backus-Naur form I describe the sintax of the language, but what type of approaches it is convenient to use to providing a formal semantics of this type of programming language (denotational, axiomatic or operational). $\endgroup$ – Claudio Biale Feb 18 '13 at 21:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.