formalsemantics

   1 INTERPOL - ANTICS
   2 +++++++++++++++++
   3
   4
   5
   6 <e,o> |> v  means that e evaluates to v in the state o.
   7
   8
   9
  10
  11 basic arithmetic operations.
  12
  13 (PLUS)
  14 <e1 + e2, o> |> v   <=   <e1,o> |> v1  &  <e2,o> |> v2  &  v is the sum of v1 and v2
  15
  16
  17 (MINUS)
  18 <e1 - e2, o> |> v   <=   <e1,o> |> v1  &  <e2,o> |> v2  &  v is v1 subtracted from v2
  19
  20
  21 (MULT)
  22 <e1 * e2, o> |> v   <=   <e1,o> |> v1  &  <e2,o> |> v2  &  v is the product of v1 and v2
  23
  24
  25 (DIV)
  26 <e1 / e2, o> |> v   <=   <e1,o> |> v1  &  <e2,o> |> v2  &  v is v1 divided by v2
  27
  28
  29
  30 basic comparative operations.
  31
  32
  33 (Less Than)
  34
  35 <e1 < e2, o> |> true   <=  <e1,o> |> v1  & <e2,o> |> v2  &  v1 is smaller than v2
  36 <e1 < e2, o> |> false  <=  <e1,o> |> v1  & <e2,o> |> v2  &  v1 is larger than or as large as v2
  37
  38 <e1 <= e2, o> |> true   <=  <e1,o> |> v1  & <e2,o> |> v2  &  v1 is smaller than or as small as v2
  39 <e1 <= e2, o> |> false  <=  <e1,o> |> v1  & <e2,o> |> v2  &  v1 is larger than v2
  40
  41 +similar rules apply for greater than+
  42
  43
  44 (Equal, Not Equal)
  45
  46 <e1 == e2, o> |> true   <=  <e1,o> |> v1  & <e2,o> |> v2  &  v1 is equal to v2
  47 <e1 == e2, o> |> false  <=  <e1,o> |> v1  & <e2,o> |> v2  &  v1 is not equal to v2
  48
  49 <e1 != e2, o> |> true   <=  <e1,o> |> v1  & <e2,o> |> v2  &  v1 is not equal to to v2
  50 <e1 != e2, o> |> false  <=  <e1,o> |> v1  & <e2,o> |> v2  &  v1 is equal to v2
  51
  52
  53
  54 (Not, Neg)
  55
  56 <!e, o> |> false  <=  <e,o> |> true
  57 <!e, o> |> true   <=  <e,o> |> false
  58
  59 <-e, o> |> v2  <=  <e,o> |> v1  &  v2 is the negative value of v1
  60
  61
  62
  63
  64 (Int)
  65 <n,o> |> n  <=
  66
  67 (Bool)
  68 <b,o> |> b  <=
  69
  70
  71
  72
  73
  74 (If)
  75 <if e s1 else s2, o> |> o'   <=   <e,o> |> true  &  <s1, o> |> o'
  76 <if e s1 else s2, o> |> o'   <=   <e,o> |> false  &  <s2, o> |> o'
  77
  78 (While)
  79 <while e s, o> |> o'' <=   <e,o> |> true  &  <s,o> |> o'  &  <while e s, o'> |> o''
  80 <while e s, o> |> o   <=   <e,o> |> false
  81
  82 (Assign)
  83 <x = e, o> |> o[x->v]   <=   <e,o> |> v
  84
  85 (Seq)
  86 <s1; s2, o> |> o''   <=   <s1,o> |> o'  &  <s2, o'> |> o''