Lively Walk-Through

Live and Formal


View on GitHub

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.

Screenshot of Lively Walk-Through

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.

One field is placed in Workbench

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

change name menu

You type a new name. For example, UnitPrice.

change name menu

The field widget is now named UnitPrice.

change name menu

Repeat this operation to build the GUI.

all widgets placed

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.

VDM Browser

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.

VDM spec

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 Browser

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.

Livetalk Browser

Testdriving the prototype

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

using the prototype

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

result

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)

plot widget