Quelle IO.vdmrt Sprache: VDM

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

quality92%

¤ Dauer der Verarbeitung: 0.23 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.