Lively Walk-Through

Lively Walk-Through is a GUI prototyping environment where UI designers and VDM engineers collaborate to integrate UI design and functional design.

Placing widgets

Let’s build a simple calculator which computes the total price from unit price and amount.

First, you build a prototypical GUI for it. The left side is Workbench where you build a GUI, and the right is a list of widgets. You can drag and drop a field widget into Workbench.

Then, You rename the widget by selecting name->change name in the context menu of the field widget.

You type a new name. For example, UnitPrice.

The field widget is now named UnitPrice.

Repeat this operation to build the GUI.

Once you are satisfied with the prototypical GUI, fix position of the widgets by selecting fix position in the context menu.

Writing a VDM specification

Then, you give the functional specification to the prototype.

The VDM tab on the top right will bring the VDM Browser in front.

Please read (the VDM Browser section)[VDMBrowser.md] to learn how to use the browser.

The specification to compute total from unit price and amount is simple.

functions
  total : int * int -> int
  total(unit, amount) == unit * amount;

Type the specification above into the specification pane and accept it. You may test the specification on Workspace.

Binding the GUI and VDM in Livetalk

Now you have a GUI and a functional specification. You need to bind them together to obtain a working prototype.

Clicking on the Livetalk tab will bring Livetalk Browser in front.

Livetalk is a scripting language that associates an event on a widget with a series of actions. The syntax is simple.

<livetalk> ::= 
  <widget name>`<event name><cr>        /* widget and event that triggers the actions defined below */
    [<action>(<cr><action>)*]<cr>*      /* actions are separated by <cr> */
    
<action> ::= 
    <expression> |                        /* evaluate the expression */
    <expression> -> [<widget name>] |     /* feed the value of the expression to the widget */
    ! <expression>                        /* show the value of the expression in a dialog */
<expression> ::=
    <operation name>(<expression>,...) |  /* call a VDM operation */
    [<widget name>]                       /* read the value that the widget holds */
    "string"                              /* string of valid VDM expressions */

For the simple calculator, the below script will compute the total.

Calc`clicked
  total( [UnitPrice] , [Amount] ) -> [Total]

The script will evaluate a VDM operation call with the arguments from the two field widgets (UnitPrice and Amount) and then give the resulting value to the Total widget.

Testdriving the prototype

Your prototype is ready to go. Fill the UnitPrice and Amount in and then click on the Calc button.

The result will hopefully be displayed as you expect :smile:

Drawing charts

The plot widget can be used to plot data given either of the followings.

• a number
• a sequence of numbers
• a point (real*real)
• a sequence of points (seq (real*real))
• a mapping from number to number (map real to real)