Examples: Basic Functions

isConcreteElementOf_Int
val a = 1
val b = Intervals(IntegerVal(0), IntegerVal(10)
val c = Intervals.Positive
val d = Intervals.Negative

isConcreteElementOf_Int(a, b) = true

isConcreteElementOf_Int(a, c) = true

isConcreteElementOf_Int(a, d) = false

---

isConcreteElementOf_List
val list1 = List(1,2,3)
val list2 = List()
val a = Intervals(IntegerVal(0), IntegerVal(10)
val b = Intervals.Positive
val d = Intervals.Negative

isConcreteElementOf_List(list1, ANil) = false

isConcreteElementOf_List(list2, ANil) = true

isConcreteElementOf_List(list1, Many(a)) = true

isConcreteElementOf_List(list1, Many(b)) = true

isConcreteElementOf_List(list2, Many(b)) = false

isConcreteElementOf_List(list1, Many(d)) = false

isConcreteElementOf_List(list1, Cons(a, ANil)) = false

isConcreteElementOf_List(list1, Cons(a,AMany(a))) = true

isConcreteElementOf_List(list1, Cons(a,AMany(b))) = true

isConcreteElementOf_List(list1, Cons(a,AMany(d))) = false

isConcreteElementOf_List(list1, Cons(d,AMany(b))) = false

isConcreteElementOf_List(list1, Cons(a, Cons(b, AMany(d)))) = true //widening

isConcreteElementOf_List(list1, Cons(a, Cons(b, ACons(,)))) = true //memoization

---

aHead
val a = Intervals(IntegerVal(0), IntegerVal(10)

aHead(ANil) = ANone

aHead(ACons(a,_)) = ASome(a)

aHead(AMaybe(a)) = AMaybe(a)

---

aTail
val a = Intervals(IntegerVal(0), IntegerVal(10)

aTail(ANil) = ANone

aTail(ACons(_,ANone)) = ANone

aTail(ACons(,ACons(,t))) = ASome(Interval(IntegerNegInf, IntegerInf))

aTail(ACons(_,Many(a))) = AMaybe(a)

aTail(AMaybe(a)) = AMaybe(a)

---

aLength
aLength(ANil) = ANone

aLength(ACons(,))= ASome(Interval(IntegerVal(1), IntegerInf))

aLength(AMany(_)) = ASome(Interval(IntegerVal(0), IntegerInf))