What are constraints in static semantic?

Question

In regards to model driven software development. As far as I know does the static semantic define the criteria for a model to be well-formed.

However I can't think of any real examples. So what are some real-world examples to help me better understand it?

Answer 1

Static Semantics can indeed be regarded as 'the criteria for a model to be well-formed'. What those criteria are completely depends on the (modelling) language it is describing.

Static Semantics is closely related to type-checking. With the phrase 'Static Semantics' we usually mean a formal description of the criteria that make a program/model well-formed, while a type-checking is an executable implementation of such a description, which can be used to validate actual models.

To provide an example, imagine a language with a syntactic constructs Expr.Plus = Expr "+" Expr. A possible rule (written informally) validating the well-formedness could be:

If (e1 is well-formed with type Num()) and (e2 is well-formed with type Num()), then Plus(e1, e2) is well-formed with type Num().

A more complex example of such a rule is: If (c is well-formed with type Bool()) and (e1 is well-formed with type T (where T is a type variable, not a concrete type)) and (e2 is well-formed with type T), then If(c, e1, e2) is well-typed with type T.

For a better introduction to this style of writing semantics (including formallish notation), see e.g. these slides (especially from 35)

However, static semantics can be much broader than only checking addition expressions. Imagine a modelling language that models the heating installation of a building. A rule in its semantics could specify that a model is well-formed only if all valve ends are connected (so no leaks are possible).

Moreover, static semantics differs from a grammar by the fact that it usually includes non-local/context-sensitive constraints/checks (e.g. name resolution).

Finally static semantics is different from dynamic semantics in the way that the latter describes how to compute a value from a (well-formed) model.