Eclipse Xtext - XSemantics

Why XSemantics?

The XSemantics website on Souceforge describes XSemantics like this:

"XSemantics is a DSL (implemented in Xtext itself) for writing type systems, reduction rules, interpreters (and in general relation rules) for languages implemented in Xtext. It then generates Java code that can be used in your language implemented in Xtext for scoping and validation (it can also generate a validator in Java)."

After reading this it is still not entirely clear to me exactly what XSemantics is, however, looking at the examples I can see that it is very powerful and potentially very useful.

It does not help that (to quote from the documentation) "XSemantics is thought to be used by people who are at least a little familiar with formal type systems and operational semantics". This appears to limit the potential users of what looks like useful software.

When I look at XSemantics it seems to me that it might be explainable to a wider audience as a rule based system, but we might expect rules to have the form:

if some predicate then some conclusion

like this:

if the current node is NumberLiteral then the current node is of type IntType.
Which in XSemantics is written:
axiom NumeralLiteral
    G |- NumberLiteral num : 
        ExpressionsFactory::eINSTANCE.createIntType

Another example is:

if the current node is MultiOrDiv and left is intType and right is intType then the current node is of type IntType.
Which in XSemantics is written:
rule MultiOrDiv
    G |- MultiOrDiv multiOrDiv : IntType intType
from {
    G |- multiOrDiv.left : intType
    G |- multiOrDiv.right : intType
}
      

As far as I can see, it appears to be doing a pattern search on the rule:

G |- MultiOrDiv

to check if this is a MultiOrDiv node, if so, multiOrDiv holds this instance.

Then all the conditions in the from part are checked. If they are all true then the right hand part of the rule is returned.

patern match

Relationship to Mathematical Logic and Type Theory

Since XSemantics uses mathematical logic it might be useful to try to describe the above in these terms.

If we have the situation where, if A is true and B is true then A/\B is true, the usual notation is shown on the right:

A B
A/\B

We may require that this is only true in a certain context, to emphasise this in a more precise way we can write:

G |- A G |- B
G |- A /\ B

More on these pages:

Installing XSemantics

For information about installing XSemantics see page here.


metadata block
see also: itemis blog
Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.