Specifikation of operation in VDM++

157 views Asked by At

I would like to know what the operations mean in the picture. Most what the line, 'getStartPrice()== (return startPrice)' mean.

I'm really new too this.

enter image description here

1

There are 1 answers

1
Nick Battle On

The "getStartPrice() ==" line defines the action of the operation. What may be a surpise is that an operation (or function) definition starts with two lines. The first line defines the type signature, like "op: nat * nat ==> nat", and the second line names the parameters, like "op(a, b) == ...". The body of the operation can then follow after the "==", unless it is implicit.