Ignore:
Timestamp:
Feb 9, 2011, 11:49:17 AM (9 years ago)
Author:
campbell
Message:

Port Clight semantics to the new-new matita syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Floats.ma

    r3 r487  
    2424include "Integers.ma".
    2525
    26 naxiom float: Type.
     26axiom float: Type[0].
    2727
    2828(*Module Float.*)
    2929
    30 naxiom Fzero: float.
    31 naxiom Fone: float.
     30axiom Fzero: float.
     31axiom Fone: float.
    3232
    33 naxiom Fneg: float → float.
    34 naxiom Fabs: float → float.
    35 naxiom singleoffloat: float → float.
    36 naxiom intoffloat: float → int.
    37 naxiom intuoffloat: float → int.
    38 naxiom floatofint: int → float.
    39 naxiom floatofintu: int → float.
     33axiom Fneg: float → float.
     34axiom Fabs: float → float.
     35axiom singleoffloat: float → float.
     36axiom intoffloat: float → int.
     37axiom intuoffloat: float → int.
     38axiom floatofint: int → float.
     39axiom floatofintu: int → float.
    4040
    41 naxiom Fadd: float → float → float.
    42 naxiom Fsub: float → float → float.
    43 naxiom Fmul: float → float → float.
    44 naxiom Fdiv: float → float → float.
     41axiom Fadd: float → float → float.
     42axiom Fsub: float → float → float.
     43axiom Fmul: float → float → float.
     44axiom Fdiv: float → float → float.
    4545
    46 naxiom Fcmp: comparison → float → float → bool.
     46axiom Fcmp: comparison → float → float → bool.
    4747
    48 naxiom eq_dec: ∀f1,f2: float. (f1 = f2) + (f1 ≠ f2).
     48axiom eq_dec: ∀f1,f2: float. (f1 = f2) + (f1 ≠ f2).
    4949
    5050(* * Below are the only properties of floating-point arithmetic that we
    5151  rely on in the compiler proof. *)
    5252
    53 naxiom addf_commut: ∀f1,f2. Fadd f1 f2 = Fadd f2 f1.
     53axiom addf_commut: ∀f1,f2. Fadd f1 f2 = Fadd f2 f1.
    5454
    55 naxiom subf_addf_opp: ∀f1,f2. Fsub f1 f2 = Fadd f1 (Fneg f2).
     55axiom subf_addf_opp: ∀f1,f2. Fsub f1 f2 = Fadd f1 (Fneg f2).
    5656
    57 naxiom singleoffloat_idem:
     57axiom singleoffloat_idem:
    5858  ∀f. singleoffloat (singleoffloat f) = singleoffloat f.
    5959
    60 naxiom Fcmp_ne_eq:
     60axiom Fcmp_ne_eq:
    6161  ∀ f1,f2. Fcmp Cne f1 f2 = ¬(Fcmp Ceq f1 f2).
    62 naxiom Fcmp_le_lt_eq:
     62axiom Fcmp_le_lt_eq:
    6363  ∀ f1,f2. Fcmp Cle f1 f2 = (Fcmp Clt f1 f2 ∨ Fcmp Ceq f1 f2).
    64 naxiom Fcmp_ge_gt_eq:
     64axiom Fcmp_ge_gt_eq:
    6565  ∀f1,f2. Fcmp Cge f1 f2 = (Fcmp Cgt f1 f2 ∨ Fcmp Ceq f1 f2).
    6666
    67 naxiom Feq_zero_true: Fcmp Ceq Fzero Fzero = true.
    68 naxiom Feq_zero_false: ∀f. f ≠ Fzero → Fcmp Ceq f Fzero = false.
     67axiom Feq_zero_true: Fcmp Ceq Fzero Fzero = true.
     68axiom Feq_zero_false: ∀f. f ≠ Fzero → Fcmp Ceq f Fzero = false.
    6969
    7070(*End Float.*)
Note: See TracChangeset for help on using the changeset viewer.