Re: [isabelle] Real time in generated code

Hi Marco,

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 ().

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