VDM++

Go to M+ homepage

Values

Click an attribute element.
Select the Base tab.
Select "true” in the ReadOnly.

VDM++ Example Code

class Foo

types

-- ˅

-- ˄

values

public LIMIT : Int = 100;

-- ˅

-- ˄

instance variables

-- ˅

-- ˄

functions

-- ˅

-- ˄

operations

-- ˅

-- ˄

sync

-- ˅

-- ˄

thread

-- ˅

-- ˄

end Foo

Functions

Apply to the operations that generate the partial functions or the total functions.

Click an operation element.
Select the Stereotype tab.
Enter "function" or “total_function” in the Name. For the partial functions, enter “function”. For the total functions, enter “total_function”.

VDM++ Example Code

class Foo

types

-- ˅

-- ˄

values

-- ˅

-- ˄

instance variables

-- ˅

-- ˄

functions

public calc : () -> ()

calc() ==

-- ˅

is not yet specified

pre

post

-- ˄

;

-- ˅

-- ˄

operations

-- ˅

-- ˄

sync

-- ˅

-- ˄

thread

-- ˅

-- ˄

end Foo

Invariants, Preconditions, Postconditions

Write invariants, preconditions, and postconditions in the User Code Area - which is an area quoted with “˅” and “˄”.

VDM++ Example Code

class Foo

types

-- ˅

-- ˄

values

-- ˅

-- ˄

instance variables

public sum : nat;

-- ˅

-- ˄

functions

-- ˅

-- ˄

operations

public increment : () ==> ()

increment() ==

-- ˅

sum := sum + 1;

post sum = sum~ + 1;

-- ˄

;

-- ˅

-- ˄

sync

-- ˅

-- ˄

thread

-- ˅

-- ˄

end Foo

Generate set/sequence types from the associations

Using TaggedValue

Click an association element.
Select the TaggedValue tab.
Enter "collection_kind" in the Name, and set/sequence types in the Value. The following set/sequence types can be entered. If this TaggedValue is not set, it is the same as setting "set".
- set
- set1
- seq
- seq1
Select the Association End tab.
Enter “*” for the upper limit in the Multiplicity.

VDM++ Example Code

class Foo

types

-- ˅

-- ˄

values

-- ˅

-- ˄

instance variables

private bars : seq of Bar;

-- ˅

-- ˄

functions

-- ˅

-- ˄

operations

-- ˅

-- ˄

sync

-- ˅

-- ˄

thread

-- ˅

-- ˄

end Foo

Using Stereotype

Click an association element.
Select the Stereotype tab.
Enter "collection_kind=(set/sequence type)" in the Name. The following set/sequence types can be entered. If this Stereotype is not set, it is the same as setting "set".
- set
- set1
- seq
- seq1
Select the Association End tab.
Enter “*” for the upper limit in the Multiplicity.

VDM++ Example Code

class Foo

types

-- ˅

-- ˄

values

-- ˅

-- ˄

instance variables

private bars : seq of Bar;

-- ˅

-- ˄

functions

-- ˅

-- ˄

operations

-- ˅

-- ˄

sync

-- ˅

-- ˄

thread

-- ˅

-- ˄

end Foo

Generate map types from the qualified associations

Using TaggedValue

Click an association element with the qualifier.
Select the TaggedValue tab.
Enter "collection_kind" in the Name and a collection type in the Value. The following collection types can be entered. If this TaggedValue is not set, it is the same as setting "map".
- map
- inmap

VDM++ Example Code

class Foo

types

-- ˅

-- ˄

values

-- ˅

-- ˄

instance variables

private bars : inmap nat to Bar;

-- ˅

-- ˄

functions

-- ˅

-- ˄

operations

-- ˅

-- ˄

sync

-- ˅

-- ˄

thread

-- ˅

-- ˄

end Foo

Using Stereotype

Click an association element with the qualifier.
Select the Stereotype tab.
Enter "collection_kind=(Collection type)" in the Name. The following collection types can be entered. If this Stereotype is not set, it is the same as setting "map".
- map
- inmap

VDM++ Example Code

class Foo

types

-- ˅

-- ˄

values

-- ˅

-- ˄

instance variables

private bars : inmap nat to Bar;

-- ˅

-- ˄

functions

-- ˅

-- ˄

operations

-- ˅

-- ˄

sync

-- ˅

-- ˄

thread

-- ˅

-- ˄

end Foo

VDM++

Contents

Values

Functions

Invariants, Preconditions, Postconditions

Generate set/sequence types from the associations

Generate map types from the qualified associations