INTERPOL - ANTICS
+++++++++++++++++



<e,o> |> v  means that e evaluates to v in the state o.




basic arithmetic operations.

(PLUS)
<e1 + e2, o> |> v   <=   <e1,o> |> v1  &  <e2,o> |> v2  &  v is the sum of v1 and v2


(MINUS)
<e1 - e2, o> |> v   <=   <e1,o> |> v1  &  <e2,o> |> v2  &  v is v1 subtracted from v2


(MULT)
<e1 * e2, o> |> v   <=   <e1,o> |> v1  &  <e2,o> |> v2  &  v is the product of v1 and v2


(DIV)
<e1 / e2, o> |> v   <=   <e1,o> |> v1  &  <e2,o> |> v2  &  v is v1 divided by v2



basic comparative operations.


(Less Than)

<e1 < e2, o> |> true   <=  <e1,o> |> v1  & <e2,o> |> v2  &  v1 is smaller than v2
<e1 < e2, o> |> false  <=  <e1,o> |> v1  & <e2,o> |> v2  &  v1 is larger than or as large as v2

<e1 <= e2, o> |> true   <=  <e1,o> |> v1  & <e2,o> |> v2  &  v1 is smaller than or as small as v2
<e1 <= e2, o> |> false  <=  <e1,o> |> v1  & <e2,o> |> v2  &  v1 is larger than v2

+similar rules apply for greater than+


(Equal, Not Equal)

<e1 == e2, o> |> true   <=  <e1,o> |> v1  & <e2,o> |> v2  &  v1 is equal to v2
<e1 == e2, o> |> false  <=  <e1,o> |> v1  & <e2,o> |> v2  &  v1 is not equal to v2

<e1 != e2, o> |> true   <=  <e1,o> |> v1  & <e2,o> |> v2  &  v1 is not equal to to v2
<e1 != e2, o> |> false  <=  <e1,o> |> v1  & <e2,o> |> v2  &  v1 is equal to v2



(Not, Neg)

<!e, o> |> false  <=  <e,o> |> true
<!e, o> |> true   <=  <e,o> |> false

<-e, o> |> v2  <=  <e,o> |> v1  &  v2 is the negative value of v1




(Int)
<n,o> |> n  <=

(Bool)
<b,o> |> b  <=





(If)
<if e s1 else s2, o> |> o'   <=   <e,o> |> true  &  <s1, o> |> o'
<if e s1 else s2, o> |> o'   <=   <e,o> |> false  &  <s2, o> |> o'

(While)
<while e s, o> |> o'' <=   <e,o> |> true  &  <s,o> |> o'  &  <while e s, o'> |> o''
<while e s, o> |> o   <=   <e,o> |> false

(Assign)
<x = e, o> |> o[x->v]   <=   <e,o> |> v

(Seq)
<s1; s2, o> |> o''   <=   <s1,o> |> o'  &  <s2, o'> |> o''