Quelle  CSV.vdmrt

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