• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Oslib
      • File-types
      • Get-decoded-time$
        • Time-zone-abbreviation
        • Time-zone-to-utc-string
      • Argv
      • Copy
      • Catpath
      • Ls
      • Universal-time
      • Tempfile
      • Basename
      • Dirname
      • Copy!
      • Ls-files
      • Mkdir
      • Date
      • Rmtree
      • Lisp-version
      • Lisp-type
      • Ls-subdirs
      • Getpid
      • Dirnames
      • Basenames
      • Basename!
      • Ls-subdirs!
      • Ls-files!
      • Dirname!
      • Ls!
      • Catpaths
      • Mkdir!
      • Rmtree!
      • Remove-nonstrings
    • Std/io
    • Bridge
    • Clex
    • Tshell
    • Unsound-eval
    • Hacker
    • ACL2s-interface
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Oslib

Get-decoded-time$

Get the current time represented as a decoded time.

Signature

(get-decoded-time$ state) 
  → 
(mv second minute hour date month year day daylight-p zone state)

Returns

second — Type (natp second).

minute — Type (natp minute).

hour — Type (natp hour).

date — Type (posp date).

month — Type (posp month).

year — Type (integerp year).

day — Type (natp day).

zone — Type (rationalp zone).

state — Type (state-p1 state), given (force (state-p1 state)).

This is a wrapper to the standard get-decoded-time Common Lisp function. In the logic, this is modeled as a read from the ACL2 oracle.

There are nine return values in addition to state:

• second — A natural number less than 60.
• minute — A natural number less than 60.
• hour — A natural number less than 24.
• date — A positive integer less than 32. This represents the day of the month.
• month — A positive integer less than 13. January is 1, February is 2, etc.
• year — An integer number representing the year A.D.
• day — A natural number less than 7. This represents the day of the week. Monday is 0, Tuesday is 1, etc.
• daylight-p — A generalized boolean indicating whether daylight savings time is active.
• zone — A rational number between -24 and 24 (inclusive). This represents the number of hours west of GMT. This value will be a multiple of 1/3600 (i.e. a granularity of one second). This value is not dependent on daylight-p. E.g., the value 6 always represents central time (either Central Standard Time or Central Daylight Time depending on daylight-p). See time-zone-abbreviation for an example of the use of this value.

See also universal-time, which returns an integer representation of the current time.

Definitions and Theorems

Function: get-decoded-time$

(defun get-decoded-time$ (state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((__function__ 'get-decoded-time$))
    (declare (ignorable __function__))
    (b* ((- (raise "Raw Lisp definition not installed?"))
         ((mv err val state)
          (read-acl2-oracle state)))
      (if (and (not err)
               (equal (len val) 9)
               (integer-range-p 0 60 (first val))
               (integer-range-p 0 60 (second val))
               (integer-range-p 0 24 (third val))
               (integer-range-p 1 32 (fourth val))
               (integer-range-p 1 13 (fifth val))
               (integerp (sixth val))
               (integer-range-p 0 7 (seventh val))
               (rationalp (ninth val))
               (<= -24 (ninth val))
               (<= (ninth val) 24)
               (equal (mod (ninth val) 1/3600) 0))
          (mv (first val)
              (second val)
              (third val)
              (fourth val)
              (fifth val)
              (sixth val)
              (seventh val)
              (eighth val)
              (ninth val)
              state)
        (mv 0 0 0 1 1 0 0 nil 0 state)))))

Theorem: natp-of-get-decoded-time$.second

(defthm natp-of-get-decoded-time$.second
  (b* (((mv common-lisp::?second
            ?minute ?hour ?date ?month ?year
            ?day ?daylight-p ?zone acl2::?state)
        (get-decoded-time$ state)))
    (natp second))
  :rule-classes :type-prescription)

Theorem: natp-of-get-decoded-time$.minute

(defthm natp-of-get-decoded-time$.minute
  (b* (((mv common-lisp::?second
            ?minute ?hour ?date ?month ?year
            ?day ?daylight-p ?zone acl2::?state)
        (get-decoded-time$ state)))
    (natp minute))
  :rule-classes :type-prescription)

Theorem: natp-of-get-decoded-time$.hour

(defthm natp-of-get-decoded-time$.hour
  (b* (((mv common-lisp::?second
            ?minute ?hour ?date ?month ?year
            ?day ?daylight-p ?zone acl2::?state)
        (get-decoded-time$ state)))
    (natp hour))
  :rule-classes :type-prescription)

Theorem: posp-of-get-decoded-time$.date

(defthm posp-of-get-decoded-time$.date
  (b* (((mv common-lisp::?second
            ?minute ?hour ?date ?month ?year
            ?day ?daylight-p ?zone acl2::?state)
        (get-decoded-time$ state)))
    (posp date))
  :rule-classes :type-prescription)

Theorem: posp-of-get-decoded-time$.month

(defthm posp-of-get-decoded-time$.month
  (b* (((mv common-lisp::?second
            ?minute ?hour ?date ?month ?year
            ?day ?daylight-p ?zone acl2::?state)
        (get-decoded-time$ state)))
    (posp month))
  :rule-classes :type-prescription)

Theorem: integerp-of-get-decoded-time$.year

(defthm integerp-of-get-decoded-time$.year
  (b* (((mv common-lisp::?second
            ?minute ?hour ?date ?month ?year
            ?day ?daylight-p ?zone acl2::?state)
        (get-decoded-time$ state)))
    (integerp year))
  :rule-classes :type-prescription)

Theorem: natp-of-get-decoded-time$.day

(defthm natp-of-get-decoded-time$.day
  (b* (((mv common-lisp::?second
            ?minute ?hour ?date ?month ?year
            ?day ?daylight-p ?zone acl2::?state)
        (get-decoded-time$ state)))
    (natp day))
  :rule-classes :type-prescription)

Theorem: rationalp-of-get-decoded-time$.zone

(defthm rationalp-of-get-decoded-time$.zone
  (b* (((mv common-lisp::?second
            ?minute ?hour ?date ?month ?year
            ?day ?daylight-p ?zone acl2::?state)
        (get-decoded-time$ state)))
    (rationalp zone))
  :rule-classes :type-prescription)

Theorem: state-p1-of-get-decoded-time$.state

(defthm state-p1-of-get-decoded-time$.state
  (implies (force (state-p1 state))
           (b* (((mv common-lisp::?second
                     ?minute ?hour ?date ?month ?year
                     ?day ?daylight-p ?zone acl2::?state)
                 (get-decoded-time$ state)))
             (state-p1 state)))
  :rule-classes :rewrite)

Theorem: get-decoded-time$.second-linear

(defthm get-decoded-time$.second-linear
  (b* (((mv common-lisp::?second
            ?minute ?hour ?date ?month ?year
            ?day ?daylight-p ?zone acl2::?state)
        (get-decoded-time$ state)))
    (<= second 59))
  :rule-classes :linear)

Theorem: get-decoded-time$.minute-linear

(defthm get-decoded-time$.minute-linear
  (b* (((mv common-lisp::?second
            ?minute ?hour ?date ?month ?year
            ?day ?daylight-p ?zone acl2::?state)
        (get-decoded-time$ state)))
    (<= minute 59))
  :rule-classes :linear)

Theorem: get-decoded-time$.hour-linear

(defthm get-decoded-time$.hour-linear
  (b* (((mv common-lisp::?second
            ?minute ?hour ?date ?month ?year
            ?day ?daylight-p ?zone acl2::?state)
        (get-decoded-time$ state)))
    (<= hour 23))
  :rule-classes :linear)

Theorem: get-decoded-time$.date-linear

(defthm get-decoded-time$.date-linear
  (b* (((mv common-lisp::?second
            ?minute ?hour ?date ?month ?year
            ?day ?daylight-p ?zone acl2::?state)
        (get-decoded-time$ state)))
    (<= date 31))
  :rule-classes :linear)

Theorem: get-decoded-time$.month-linear

(defthm get-decoded-time$.month-linear
  (b* (((mv common-lisp::?second
            ?minute ?hour ?date ?month ?year
            ?day ?daylight-p ?zone acl2::?state)
        (get-decoded-time$ state)))
    (<= month 12))
  :rule-classes :linear)

Theorem: get-decoded-time$.day-linear

(defthm get-decoded-time$.day-linear
  (b* (((mv common-lisp::?second
            ?minute ?hour ?date ?month ?year
            ?day ?daylight-p ?zone acl2::?state)
        (get-decoded-time$ state)))
    (<= day 6))
  :rule-classes :linear)

Theorem: get-decoded-time$.zone-min-linear

(defthm get-decoded-time$.zone-min-linear
  (b* (((mv common-lisp::?second
            ?minute ?hour ?date ?month ?year
            ?day ?daylight-p ?zone acl2::?state)
        (get-decoded-time$ state)))
    (<= -24 zone))
  :rule-classes :linear)

Theorem: get-decoded-time$.zone-max-linear

(defthm get-decoded-time$.zone-max-linear
  (b* (((mv common-lisp::?second
            ?minute ?hour ?date ?month ?year
            ?day ?daylight-p ?zone acl2::?state)
        (get-decoded-time$ state)))
    (<= zone 24))
  :rule-classes :linear)

Theorem: mod-of-get-decoded-time$.zone-and-1/3600

(defthm mod-of-get-decoded-time$.zone-and-1/3600
  (b* (((mv common-lisp::?second
            ?minute ?hour ?date ?month ?year
            ?day ?daylight-p ?zone acl2::?state)
        (get-decoded-time$ state)))
    (equal (mod zone 1/3600) 0)))

Subtopics

Time-zone-abbreviation

Convert a time zone to an abbreviation string.

Time-zone-to-utc-string

Convert a time zone to a UTC offset string.