| products/sources/formale sprachen/PVS/orders/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: Test.txt Sprache: Unknown
|
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 [ Verzeichnis aufwärts0.6unsichere Verbindung Übersetzung europäischer Sprachen durch Browser ] |