|
class IO
-- Overture STANDARD LIBRARY: INPUT/OUTPUT
-- --------------------------------------------
-- Version 1.0.0
--
-- Standard library for the Overture 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 customizable.
-- Don't 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').
--
-- File path:
-- * An absolute path is accepted and used as specified.
-- * A relative path is relative to the debugger or if running in the
-- Overture IDE relative to the project root.
--
types
/**
* The file directive used in in/out functions.
*/
public filedirective = <start>|<append>
functions
/**
* Write VDM value in ASCII format to the console.
*
* @param val the VDM value to be written
* @return true if successful else false
*/
public static writeval[@p]: @p -> bool
writeval(val)==
is not yet specified;
/**
* Write VDM value in ASCII format to file. The type of the val must be
* specified as fwriteval[seq of char](...) when calling the function.
*
* @param filename the name of the file
* @param val the VDM value to be written.
* @param fdir if <start> then it will overwrite an existing file,
* else <append> will append output to the existing file
* @return true if successful else false
*/
public static fwriteval[@p]:seq1 of char * @p * filedirective -> bool
fwriteval(filename,val,fdir) ==
is not yet specified;
/**
* Read VDM value in ASCII format from file. The type which should be read must be
* specified as freadval[seq of char](...) when calling the function.
*
* @param filename the name of the file
* @return mk_(success,@p) if successful success will be
* set to true else false. @p will hold nil if unsuccessful or the value read.
*/
public static freadval[@p]:seq1 of char -> bool * [@p]
freadval(filename) ==
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.
*
* @param text the text to write to the console
* @return if successful true else false.
*/
public echo: seq of char ==> bool
echo(text) ==
fecho ("",text,nil);
/**
* Write text to file like <code>echo</code>.
*
* @param filename the name of the file
* @param text the text to write to be written.
* @param fdir if nil or <start> then it will overwrite an existing file,
* else <append> will append output to the existing file.
* @return true if successful else false
*/
public fecho: seq of char * seq of char * [filedirective] ==> bool
fecho (filename,text,fdir) ==
is not yet specified
pre filename = "" <=> fdir = nil;
/**
* Returns the last error which may have occurred by any of the io/out functions
*
* @return the last error message
*/
public ferror:() ==> seq of char
ferror () ==
is not yet specified;
-- New simplified format printing operations
/**
* Prints any VDM value to the console
*
* @param arg a VDM value of any type
*/
public static print: ? ==> ()
print(arg) ==
is not yet specified;
/**
* Prints any VDM value to the console as a new line
*
* @param arg a VDM value of any type
*/
public static println: ? ==> ()
println(arg) ==
is not yet specified;
/**
* Prints any VDM value to the console
*
* @param format standard format string used in
* Java by <code>String.format(format, value)</code>,
* though note that only the %s conversion is supported.
* eg. <code>printf("Hello [%2$-5s][%1$5s]\n", [123, {2}])</code>
* would produce <code>Hello [{2} ][ 123]</code> and a newline.
*
* @param arg a sequence of VDM values of any type
*/
public static printf: seq of char * seq of ? ==> ()
printf(format, args) ==
is not yet specified;
end IO
[ Seitenstruktur0.9Drucken
etwas mehr zur Ethik
]
|
