CODEWITHSUNDEEP
compiler-errorsvdm++vdm-sl
cxsid
cxsid

Reputation: 1

Correction & filling the missing functions in VDM-SL

Task 1: The figure below shows an incomplete set of VDM-SL specifications for the IncubatorMonitor System. The specifications also contain grammatical, typographical and logical errors.

# values

# MAX_TEMP : int = 10;

# MIN_TEMP : int = -10;

# 

# state IncubatorMonitor

# temp: int

# inv mk_IncubatorMonitor(t) == t \>= MIN_TEMP and t \<= MAX_TEMP

# init IM == mk_IncubatorMonitor(5)

# end

# 

# operations

# Increment : () ==\> ()

# Increment () ==

# (temp := temp + 1)

# pre temp \< MAX_TEMP

# post temp = temp\~ + 1

Using VDMTools to: • Correct existing errors • Fill in the missing functions

I tried running it in VDM-SL, it gave me 2 errors but I couldn't add new stuff.

Upvotes: 0

Views: 25

Answers (1)

Nick Battle
Nick Battle

Reputation: 703

VDMTools is quite an old environment and does not let you directly edit the specification unless you configure a text editor to use.

You might have more luck with VDM-VSCode?

Upvotes: 0

Related Questions