[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] date function in pvsio?



Andrea,

Yes:

<PVSio> date;
==>
"Wednesday September 16 2015, 08:43:42 (GMT-5)"

<PVSio> today;
==>
"9/16/2015"

The function get_time returns a record of type Time:

Time : TYPE = [#
    second : below(60),
    minute : below(60),
    hour   : below(24),
    day    : subrange(1,31),
    month  : subrange(1,12),
    year   : nat,
    dow    : below(7), % Day of week: 0 Monday
    dst    : bool,     % Dayligth saving time?
    tz     : {x:rat| -24 <= x AND x <= 24} % Time zone
  #]

For example:

<PVSio> get_time;
==>
(# day := 16,
dow := 2,
dst := TRUE,
hour := 8,
minute := 45,
month := 9,
second := 47,
tz := 5,
year := 2015 #)

These functions are defined in the theory stdsys in the PVSio section of
the prelude. 



Cesar
--
Cesar A. Munoz, NASA <Cesar.A.Munoz@xxxxxxxx>
Web: http://shemesh.larc.nasa.gov/people/cam
NASA Langley Research Center, Bldg. 1220, Room 115 MS. 130, Hampton, VA
23681-2199, USA
Office: +1 (757) 864 1446. Fax: +1 (757) 864 4234






On 9/16/15 5:23 AM, "pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx
on behalf of Andrea Domenici"
<pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx on behalf of
Andrea.Domenici@xxxxxxxxxxxx> wrote:

>Hello!
>
>Is there a pvsio function to print the date?
>
>Thanks,
>
>andrea
>
>-- 
>Andrea Domenici
>
>Assistant Professor
>Dept. of Information Engineering (DIIEIT), University of Pisa
>Lgo. L. Lazzarino 1, I-56122 Pisa, Italy
>tel: +39 050 2217 674 fax: +39 050 2217600
>                          "Omnia sunt communia" -- Th. Müntzer
>