Additional print statements in IO library in VDM-RT

[joey-coleman]

The following bug was originally reported on Sourceforge by kgpierce, 2013-07-15 16:25:20.137000:

The IO library for VDM-RT should contain additional static operations equivalent to print/printf/println that automatically print the time before the usual console message produced by these operations. I am submitting this as an RM as I believe the standard libraries are now under the control by the LB.

1. Identification of the Originator.

   Ken Pierce

2. Target of the request: defining the affected components of the language definition.

   IO library in VDM-RT only.
   

3. Motivation for the request.
   

   The static print operations in the IO libraries (print/printf/println) for the three VDM flavours are very useful for debugging models. In VDM-RT models, where the notion of time is a built-in, it is also useful to be able to print out the exact time at which print statements occur. This can be done in the following way with the current library:

   IO`printf("[%s] Periodic operation called.\n", [time/1e9]);

   Will produce something like the following:

   [1.0E-8] Periodic operation called.
   [0.02000001] Periodic operation called.
   [0.04000001] Periodic operation called.
   [0.06000001] Periodic operation called.

   This can be quite labourious if it is repeated all over the model, especially when printf is not needed to format other variables (as in the example above). In addition, there is no real control over the formatting of the time, since printf currently only recognises %s as a formatting placeholder.
   

4. Description of the request, including:

   1. description of the modification;

      The proposal of this RM is to add three additional static operations to the IO library in VDM-RT that are equivalent to print/printf/println, but that print the time to the console in addition to the message. The suggested names will be tprint, tprintf, and tprintln. For example a call such as the following:

      IO`tprintln("Periodic operation called.");

      Will produce something like the following:

      [1.0E-8] Periodic operation called.
      [0.02000001] Periodic operation called.
      [0.04000001] Periodic operation called.
      [0.06000001] Periodic operation called.

      To handle the formatting for printing the time, the proposal is to have some default behaviour (for example, seconds without rounding as above) and to permit the user to alter this behaviour somehow. I propose the following options for this are discussed by the community.

      For where to set the format, two obvious options are:

      (a) a static operation in IO to set up the format (b) an IDE setting

      For how to set the format, two obvious options are:

      (i) permitting the user to give some kind of format string (ii) giving the user a set of predefined options, offered via quote types for option (a) above, or a dropdown box for option (b). Rxample formats could include nanoseconds ("20000010"), microseconds ("20000.01"), milliseconds ("20.00001"), seconds ("0.02000001"), hours/minutes/seconds ("00:00:0.02000001"). The possibility to set rounding to significant figures or decimal places would also be welcome in this case.

   2. benefits from the modification;

      It reduces clutter from VDM-RT models by moving often-used functionality to the standard library.

   3. possible side effects.

      None in particular. Adding additional operations maintains compatibility from VDM++ models when converting to a VDM-RT model (though not the other way round).

5. If appropriate, a test suite for validation of the modification in the executable models.

   Not applicable.

[joey-coleman]

Comment by annehax, 2013-09-06 07:27:11.982000:

The suggested operations sound useful.

[joey-coleman]

Comment by mver, 2013-09-06 11:41:34.613000:

The requester is raising two issues IMHO:

(1) currently the inability to properly format the debug output in the IO.print* functions. I fully AGREE with this observation!

(2) extend the standard library for VDM-RT only, with tprint* functions that add the wall-clock time. I DISAGREE to with this point, for two reasons: (2-a) we should keep the standard libraries consistant and identical across all language dialects when possible. The arguments for specific VDM-RT extensions are weak as: (2-b) the functionality required can easily be implemented using a single auxiliary wrapper operation at the specification level, i.e. something like:

class DoIo

instance variables count : nat := 0

operations static public printf: seq of char * seq of ? ==> () printf (pat, dat) == IO`printf("[%s] "^pat, [time/1e9]^dat);

public doit: () ==> ()
doit () == ( count := count + 1; DoIo`printf("periodic thread called %s\n", [count]))

thread periodic (1E6, 0, 0, 0) (doit)

end DoIo

Which will execute like:

\ Overture Console [1.092E-6] periodic thread called 1 [0.001001092] periodic thread called 2 [0.002001092] periodic thread called 3 [0.003001092] periodic thread called 4 [0.004001092] periodic thread called 5 [0.005001092] periodic thread called 6 [0.006001092] periodic thread called 7

Therefore, I propose to REJECT this language change and suggest to the requester to submit a language (standard library) change that allows proper formatting of the print* operations in stead.

[joey-coleman]

Comment by nicoplat, 2013-09-08 15:32:12.726000:

• status: open --> closed
• Group: Submitted --> REJECTED

[joey-coleman]

Comment by mver, 2014-02-15 22:36:15.042000:

Dear Ken,

This message is to inform you formally on the closure of your request for an Overture language modification, on additional print statements in the IO library for VDM-RT.

The language board has decided to reject your proposal, as we believe that the API of the standard library should be kept unified across the VDM dialects. We do however agree that the formatting functions in IO`printf are too restricted (now only supporting the "%s" pattern), but we believe that this should be dealt with as a normal bug report. We suggest that you submit such a report in the Overture bug tracker on github.

Thank you for submitting your proposal, if there are any further questions, please do not hesitate to contact us.

On behalf of the Overture language board, Marcel Verhoef