Checklist: Operators

AList

DONE:

• head -> aHead
• tail -> aTail
• length
• isEmpty -> isNil
• intersect -> intersect_AList
• union -> union_AList
• subset -> subset_AList
• widen -> widen_AList
• equals -> ===
• isConcreteElementOf

TODO:

• ++ (list,list)
• append (list,elem)/prepend(list, list)
• contains(elem)
• apply(f)/map(f)

---

AInt

DONE:

• integerWtoInt
• <= (not subset, i1 < i2 || i1 == i2)
• union_Interval
• contains_Interval
• intersect_Interval
• ===
• isPositive
• isNegative
• isZero
• isConcreteElementOf

TODO:

• complementSet

---

ABool

DONE:

• &&
• ||
• ===
• !==
• isConcreteElementOf
• intersect_ABool
• union_ABool
• !

TODO:

---

AOption

DONE:

• isConcreteElementOf
• union_AOption[AInt]
• union_AOption[AList]
• intersect_AOption[AInt]
• intersect_AOption[AList]
• widen_AOption[AInt]
• widen_AOption[AList]

TODO:

• contains

---

AState, AStmt and ATest

DONE:

• AState
• AStmt
  • AssignN0
  • AssignN1
  • Add1
  • Add1_ATail
  • Subtract1
  • Subtract1_ATail
  • Assign_SameValues
• ATest
  • xsIsNilTest
  • xsIsNotNil
  • nIsPositive
  • nIsNegative
  • nEqualsZero

TODO:

• AState -> include generic version
• AssignAnyN
• AddAnyN
• SubtractAnyN

---

Abstract Transformers

DONE:

• AIf
• AWhile
• AAssert

TODO:

• AAssume
• AVerify