Home

Welcome to VDMPad

VDMPad is a simple Web IDE server for VDM-SL.
VDMPad runs on MacOSX or Linux distributions. It does NOT run on Windows platforms.

Introduction

1. How to open VDMPad

If you are a mac user, please launch the VDMPad app. If you are a linux user, please run VDMPad.app/squeak.sh .
You'll see a little window like the below.

The litle window is a HTTP server on http://localhost:8085/ accepting connections from only localhost.
You can open it with your favorite browser, such as google chrome or firefox.

2. How to evaluate a VDM expression

If you open http://localhost:8085/ in your browser, the page will look like the below.

Please type "1+2" in the little text box just above the "evaluate" button. The text box is called "expression area".
By clicking the "evaluate" button, you'll see "3" in the box below the button. The lower box is called "value area".
If you made a little mistake in the expression, such as "1+'2'", an error message will appear at the bottom. The area is called "message area".

Now you can handily evaluate any VDM expression!

3. How to write a VDM specification

The large text box in the upper area is called "specification area".
As the name explains, that's where you write your specification in.
For example, the following specification will define a simple counter.

module Counter
exports all
definitions
state counter of
    count : nat
    init s == s = mk_counter(0)
end
operations
    step : () ==> nat
    step() == (count := count + 1; return count);
    current : () ==> nat
    current() == return count;
    reset : () ==> ()
    reset() == count := 0;
end Counter

Please clear the expression area if an expression is left there.
Clicking the "evaluate" button will send the specification to the server and start animation session if no error.

VDMPad gives a UI to directly manipulate the internal state of the animating specification.
In the above specification, "0" will be in the "count" variable. You can change the value by typing your favorite value in the box and press the evaluate button. If a new set of values raises a syntax error, a type error or an invariant violation, it'll be notified at the message area.

You can evaluate operation by typing an expression using an operation defined in the specification.
For example, if you type "step()" in the expression area and press the evaluate button (or cmd-p/ctrl-p), the value of the "count" variable will increment.

4. How to save a specification

Please move your mouse cursor over the little rectangle at the left top corner of the page.
A menu will appear on the left side of the IDE.
Please find an empty text box at the bottom of the menu to type a name of your specification.
By clicking a "save" button just under the text box, your specification will be saved along with the animation state.

The name will be added to the menu. If you click on a name, a specification saved with the name will be loaded.
If you click on a name, "Load", "Save", "Save&Export" and "Delete" button will appear.

The specification and animation state is stored in your browser's local storage, NOT on the server.
Please note that different browser on the same machine will have different set of "saved" specifications.

5. How to export a specification

If you want to save a specification, "Save&Export" button will start downloading the specification along with its animation state in JSON format.
The export function works with google chrome and firefox. Safari will just open a new tab with a JSON string. You need to explicitly save the content with the File/SaveAs... menu.

6. How to setup a VDMPad server for remote clients

If you want to setup a VDMPad server for remote accesses, you'll need to setup a so-called "reverse proxy" server.
One typical config of a reverse proxy is to run Apache2 server with a piece of config like below.

    <VirtualHost *:80>
    ServerName myhost.example.com
    ServerAdmin webmaster@myhost.example.com
    ProxyRequests Off
    ProxyPass / http://localhost:8085/
        <Location />
        AuthType Digest
        AuthName VDMPad
        AuthDigestDomain / http://localhost:8085/ http://myhost.example.com:80/
        AuthDigestProvider file
        AuthUserFile /path/to/digest/file/htdigest.vdmpad
        Require valid-user
        ProxyPassReverse http://localhost:8085/
        Order allow,deny
        Allow from all
        </Location>
    </VirtualHost>

7. How to ...

Many good resources for VDM are available at Overture tool.

Project Members:

• Tomohiro Oda (admin)