class IO -- VDMTools STANDARD LIBRARY: INPUT/OUTPUT -- -------------------------------------------- -- -- Standard library for the VDMTools Interpreter. When the interpreter -- evaluates the preliminary functions/operations in this file, -- corresponding internal functions is called instead of issuing a run -- time error. Signatures should not be changed, as well as name of -- module (VDM-SL) or class (VDM++). Pre/post conditions is -- fully user customisable. -- Dont care's may NOT be used in the parameter lists. -- -- The in/out functions will return false if an error occurs. In this -- case an internal error string will be set (see 'ferror'). types public filedirective = | functions -- Write VDM value in ASCII format to std out: public writeval[@p]: @p -> bool writeval(val)== is not yet specified; -- Write VDM value in ASCII format to file. -- fdir = will overwrite existing file, -- fdir = will append output to the file (created if -- not existing). public fwriteval[@p]:seq1 of char * @p * filedirective -> bool fwriteval(filename,val,fdir) == is not yet specified; -- Read VDM value in ASCII format from file public freadval[@p]:seq1 of char -> bool * [@p] freadval(f) == is not yet specified post let mk_(b,t) = RESULT in not b => t = nil; operations -- Write text to std out. Surrounding double quotes will be stripped, -- backslashed characters should be interpreted. public echo: seq of char ==> bool echo(text) == fecho ("",text,nil); -- Write text to file like 'echo' public fecho: seq of char * seq of char * [filedirective] ==> bool fecho (filename,text,fdir) == is not yet specified pre filename = "" <=> fdir = nil; -- The in/out functions will return false if an error occur. In this -- case an internal error string will be set. 'ferror' returns this -- string and set it to "". public ferror:() ==> seq of char ferror () == is not yet specified end IO