tomooda / ViennaTalk

ViennaTalk has moved to github -

ViennaTalk is a collection of libraries to support the formal specification language VDM-SL. ViennaTalk currently support animation using VDMJ and/or VDMPad server.

The documentation is available at ViennaTalk-doc page at github although it's in a very early stage :-)

VDM-SL Engine

ViennaTalk provides various mechanisms to animate VDM-SL specifications.

1. ViennaVDMJ ... runs VDMJ (Java implementation of VDM interpreter)
2. ViennaServer ... serves VDM animation via HTTP
3. ViennaClient ... requests evaluation of VDM expressions to servers via HTTP
4. ViennaBankEngine ... aggregates arbitrary number of engines to concurrently perform multiple animations

The easiest way to try VDM-SL is to use ViennaClient. ViennaClient default will use a public VDM-SL server at http://vdmpad.csce.kyushu-u.ac.jp/ .

VDMPad

VDMPad is a handy and simple Web-IDE for VDM-SL. This module provides a server of VDMPad. A public server is available at http://vdmpad.csce.kyushu-u.ac.jp/

VDMC

VDMC provides interface between Smalltak and VDM-SL. VDMC represents an animation instance that consists of specification and state. The objective of VDMC is to embed VDM-SL specification in a Smalltalk object as a specification so that some unimplemented methods can be emulated by animating its VDM-SL specification.

Lively Walk-Through

Lively Walk-Through is a UI prototyping environment where a VDM engineer and a UI designer collaborate to join their works.

Acknowledgement

Part of the ViennaTalk project is supported by Grant-in-Aid for Scientific Research (S) 24220001 from the Japan Society for the Promotion of Science.