Definitions: AList

AInt

• Is an Interval
• Form: Interval(lb, ub)

---

trait AList

• Usage: Represents the different Forms AList can have
• Forms:
  • ANil
  • ACons(head: AInt, tail: AList)
  • AMany(elem: AInt) = ANil ≀ ACons(e, Many(e))

---

trait AOption[+A]

• Usage: Exception Handling
• Forms:
  • ANone
  • ASome(_)
  • AMaybe() = ANone ≀ ASome()

---

trait ABool

• Usage: Representation of boolean values
• Forms:
  • ATrue
  • AFalse
  • (AUnknown = ATrue ≀ AFalse) -> deprecated

---

aHead(AList): AOption[AInt]

• returns the head element of an AList

---

aTail(AList): AOption[AList]

• returns the tail of an AList

---

aLength(AList): AOption[AInt]

• returns the length of an AList

---

isNil(AList): Set[ABool]

• checks whether an AList is nil or not
• cases:
  • ANil => ATrue
  • ACons => AFalse
  • AMany => ATrue, AFalse

---

isConcreteElementOf

• checks whether a concrete value is an element of an abstract value
• returns a Boolean
• Forms: List <-> AList
• Forms: Option[Int] <-> AOption[AInt]
• Forms: Option[List[Int]] <-> AOption[AList]

---

union

• symmetric operation
• returns a Set
• Forms:
  • AList, AList ->Cases:
    • ANil ∪ ANil = {ANil}
    • ANil ∪ AMany(a) = {AMany(a)}
    • ANil ∪ ACons(a,as) = {AMany(a) ∪ as} or {ANil, ACons(a, as)}
    • AMany(a) ∪ AMany(b) = {AMany(a ∪ b)}
    • AMany(a) ∪ ACons(b, bs) = {AMany(a ∪ b) ∪ bs} // //analog: ACons(a, as) ∪ Many(b)
    • ACons(a, as) ∪ ACons(b, bs) = {ACons(a ∪ b, as ∪ bs)}
  • AOption[AInt], AOption[AInt]
  • AOption[AList], AOption[AList]
  • ABool, ABool

---

intersection

• symmetric operation
• returns a Set
• Forms:
  • AList, AList -> Cases:
    • ANil ∩ ANil = {ANil}
    • ANil ∩ AMany(a) = {ANil}
    • ANil ∩ ACons(a, as) = {ANil}
    • AMany(a) ∩ AMany(b) = {AMany(a ∩ b)}
    • AMany(a) ∩ ACons(b, bs) = {ACons(a ∩ b) AMany(a) ∩ bs} //analog: ACons(a, as) ∩ Many(b)
    • ACons(a, as) ∩ ACons(b, bs) = {ACons(a ∩ b, as ∩ bs)}
  • AOption[AInt], AOption[AInt]
  • AOption[AList], AOption[AList]
  • ABool, ABool

---

subset

• equivalent: <=
• checks whether the left side of <= is a subset of the right side
• ANil is always a subset of any AList
• not symmetric

Cases:

• (ANil, ANil) = true
• (ANil, ACons(b, bs)) = true
• (ANil, AMany(b)) = true
• (ACons(a, as), ANil) = false
• (AMany(a), ANil) = false
• (AMany(a), AMany(b)) = a <= b
• (AMany(a), ACons(b, bs)) = (a <= b) && subset_AList(AMany(a), bs)
• (ACons(a as), AMany(b)) = (a <= b) && subset_AList(as, AMany(b))
• (ACons(a, as), ACons(b, bs)) = (a <= b) && subset_AList(as, bs)

---

widen

• not symmetric
  • depends on the order of the parameters
  • "temporal aspect" (e.g. loop)
• Forms:
  • AList, AList -> Cases:
    • ANil ∇ ANil = ANil
    • ANil ∇ AMany(a) = AMany(a)
    • AMany(a) ∇ ANil = AMany(a)
    • ANil ∇ ACons(a,as) = AMany(a) ∇ as
    • ACons(a,as) ∇ ANil = AMany(a) ∇ as
    • AMany(a) ∇ AMany(b) = AMany(a ∪ b)
    • AMany(a) ∇ ACons(b,bs) = AMany(a ∪ b) ∇ bs
    • ACons(b,bs) ∇ AMany(a)= AMany(a ∪ b) ∇ bs
    • ACons(a, as) ∇ ACons(b, bs) = ACons(a ∪ b, as ∇ bs)
  • AOption[AInt], AOption[AInt]
  • AOption[AList], AOption[AList]

---