Quelle CSV.vdmpp Sprache: VDM

class CSV is subclass of 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.
--

functions
/**
* Writes a seq of ? to a file in CSV format.
*
* @param filename the name of the file
* @param val the sequence of VDM values 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:seq1 of char * seq of ? * filedirective -> bool
fwriteval(filename,val,fdir) == is not yet specified;

/**
* Reads a seq of ? from a file in CSV format. The type which should be read must be
* specified as freadval[seq of char](...) when calling the function. If read is successful
* the type of @p returned is always seq of ?, where ? is any VDM type. Thus @p must always
* be set to seq of and a type.
*
* @param filename the name of the file
* @param index a index within the available lines in the file.
*   Valid range is between 1 and the value of <code>flinecount</code>.
* @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 * int -> bool * [@p]
freadval(f,index) == is not yet specified;

/**
* Gets the number of lines in a file in CSV format.
*
* @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 line count.
*/
public static flinecount: seq1 of char -> bool * int
flinecount(f) == is not yet specified;

operations
/**
* Returns the last error which may have occurred by any of the io/out functions
*
* @return the last error message
*/
public static ferror:()  ==> seq of char
ferror () ==
  is not yet specified;
end CSV

quality100%

¤ 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.