VDM-SL in Smalltalk

ViennaTalk defines three messages asViennaExpression, asViennaStatement and viennaString to evaluate and compose VDM expressions and/or statements om Smalltalk so that you can

1. start with a VDM specification,
2. implement a small fraction of it in Smalltalk,
3. gradually increase Smalltalk code that still contains some pieces of VDM expressions and/or statements, and then
4. finally you have a full implementation in Smalltalk

ViennaTalk also provides the asViennaExpressionAst and asViennaStatementAst messages to generate a VDM-SL’s abstract syntax tree (AST).

VDM Expressions in Smalltalk

A VDM expression in a String object can be evaluated by sending the asViennaExpression message.

| succ |
succ := 'lambda n:nat & n + 1' asViennaExpression.
succ value: 2

In the code above, the first line declares the variable succ. In the second line, the asViennaExpression message is sent to the string object ‘lambda n:nat & n + 1’. By sending the message, its content VDM expression is translated into a Smalltalk code and evaluated in the program context. The resulting object, which is in this case a closure object [:n | n + 1], is assigned to succ. The third line sends the value: message with actual parameter 2 to evaluate the closure object, resulting 3 (see the below screenshot).

Smalltalk variables can be referenced in VDM expressions.

| x succ |
x := 2.
succ := 'lambda n:nat & n + x' asViennaExpression.
succ value: 3

In the third line of the above code, the VDM expression lambda n:nat & n + x references the variable x, which is declared in the first line and assigned in the second line. The fourth line evaluates the expression with argument 3, resulting 5 (see the below screenshot).

VDM statements in Smalltalk

A VDM statement in a String object can be evaluated by sending the asViennaStatement message.

| x |
x := 0.
'for i in [1, 2, 3, 4, 5] do x := x + i' asViennaStatement.
x

In the code above, the string ‘for i in [1, 2, 3, 4, 5] do x := x + i’ in the third line is translated into Smalltalk and evaluated in place. The VDM for statement adds 1, 2, 3, 4, 5 to x in order. Please note that the variable x references the Smalltalk variable declared in the first line. The resulting value of the varibale x is 15 as expected.

Smalltalk object to VDM expression

In ViennaTalk, VDM values are mapped to Smalltalk objects. Each of those objects can print a VDM expression that reproduces itself.

| dic |
dic := Dictionary new.
dic at: 'key1' put: 'value1'.
dic at: 'key2' put: 'value2'.
dic

The above piece of code creates a dictionary object that maps ‘key1’ and ‘key2’ to ‘value1’ and ‘value2’ in order (see the below screenshot).

The Smalltalk’s Dictionary object are mapped to VDM’s map values. In this particular example, {“key1” |-> “value1”, “key2” |-> “value2”} is the counter part. In ViennaTalk, the corresponding VDM expression can be obtained by sending the viennaString message to an object.

| dic |
dic := Dictionary new.
dic at: 'key1' put: 'value1'.
dic at: 'key2' put: 'value2'.
dic viennaString

The result is

Generate AST

VDM expressions and statements in a String object can be parsed into ASTs by sending the asViennaExpressionAst message and the asViennaExpressionAst message in order.

For example,

'lambda n:nat & n + 1' asViennaExpressionAst

will returns its AST below.

Please note that the resulting AST is not a string object, but an instance of the ViennaNode class. The ViennaNode class represents a simple tree node with a label and arbitrary number of children. Tool developers can use this API to build their own tools that requires generating and manipulating ASTs.