search

brando90 / cs522_project

0 stars 0 forks source link

division by zero check in condition #4

Open brando90 opened 5 years ago

brando90 commented 5 years ago

we might need division by zero:

| E_ADiv : ∀ (a1 a2: aexp) (n1 n2 n3: nat),
      (a1 \\ n1) → (a2 \\ n2) → (n2 > 0) →
      (mult n2 n3 = n1) → (ADiv a1 a2) \\ n3

I notice that perhaps we need to use something like that for our code and perhaps small step was missing it?

brando90 commented 5 years ago

note:

Notation "e '\\' n"
         := (aevalR e n)
            (at level 50, left associativity)
         : type_scope.
brando90 commented 5 years ago

ok mine has an error too need to fix it later...

  (* crl < A1 / A2,Sigma > => < I1 /Int I2 > if < A1,Sigma > => < I1 > /\ < A2,Sigma > => < I2 > /\ I2 =/=Bool 0 . *)
  | BigStep_Divide: forall (A1 A2 I1 I2 : AExp ) (Sigma : State ),
    (BigStepR (B_AExpConf A1 Sigma) (B_AExpConf I1 Sigma) ) ->
    (BigStepR (B_AExpConf A2 Sigma) (B_AExpConf I2 Sigma) ) ->
    (* TODO (not (I2 = 0) ) -> *)
    (BigStepR (B_AExpConf (APlus A1 A2) Sigma) (B_AExpConf (ADiv I1 I2) Sigma)).