[M3devel] time conversion problems : Date.ToTime on AMD64_LINUX

Mika Nystrom mika at async.caltech.edu
Fri Apr 15 21:03:49 CEST 2011

"Daniel Alejandro Benavides D." writes:
>Hi all:
>although my understanding of the problem is not that good, I think there ar=
>e two routes for this abstract way one could try to prove the correctness o=
>f some implementation by setting directly instrumention code to try to see =
>for your self dynamically if you may that or what you want to see:
>This could would run with just 3 missing modules from this sources besides =
>their examples, maybe another time the HP guys allow us to see their works =
>on that:
>This package is missing from public repositories Elego too as I know, thoug=
>h they were in (see bottom links dead as of now, but, ... maybe you can loo=
>k for yourselves):
>I know some ESC/Modula-3 tries to make some inferencing of invariants, but =
>as I said it dones't mean this is totally computable, im fact in general it=
>s isn't, but it would be good to try.
>Essentially where are the codes for showing that, or are you implementing t=
>his as private code?

The problem is in DatePosix.m3 .   To reproduce, set your TZ environment variable
to Europe/London and try to convert a Date of 1970-01-01 @ 00:00:00 in the
time zone UTC to a Time.T.  You should get 0; you will get -3600.


>Thanks in advance
>--- El lun, 11/4/11, Mika Nystrom <mika at async.caltech.edu> escribi=F3:

More information about the M3devel mailing list