Re: [isabelle] Real time in generated code
as you produce Scala code, I assume that you want to have those time events in Scala.
However, Isabelle's code generator generates only a subset of what you can do in Scala,
namely the purely functional programming part. With some extension like Imperative_HOL,
you get a bit further. But for asynchronous time events, you need concurrency, and AFAIK
there's nothing like that in Isabelle at the moment. Do you want to reason about these
time events? If not, then all this is just a matter of wrapping up the generated Scala
code -- you definitely don't want to do all this in Isabelle. That is, you should write in
Scala your time trigger that evaluates the function you are interested in and outputs the
results. If you want to reason about these timing events in Isabelle, then you first have
to model all this in HOL (not easy) and adapt the code generator such that maps your model
to the Scala primitives (difficult to get really right).
Hope this helps,
On 21/01/14 02:59, marco caminati wrote:
I am using Isabelle/HOL to produce executable Scala code from suitable specifications.
I can get some code returning the value of some function upon a given argument.
However, I would also like this code to be triggered by time events at runtime.
For example, I would like the code to output its values every second.
A simple way I had in mind was to add an argument to the specification of my function representing time,
and then to plug a time counter into that argument, but I'm digressing.
In general, how do you exploit machine's clock at runtime?
Googling, I found references to timeap/timeit and to Time.now ().
1) Would any of these approaches be useful for the problem stated above?
2) I am only familiar with Isar, but I understand that to use these approaches I should embed ML code in it, right?
In this case, is there a good primer to descend from the Isar layer to the underlying ML layer?
This archive was generated by a fusion of
Pipermail (Mailman edition) and