Repository navigation
Questions
Questions:
1. Return ASome() or AMaybe(), when widened with ANil
val a = Interval(IntegerVal(-1),IntegerVal(5))
val b = Interval(IntegerVal(3),IntegerVal(8))
val c = ACons(a, ANil)
widen_Mixed(c, b)
→ widen with head of ACons (AInt), tail of ACons(ANil) and c (Interval)
→ ASome(Interval[-1,8]) union ANone → AMaybe(Interval[-1,8])
2. Recheck logic of methods
3. widen – Operator
=> widen Interval of ALists => returns AInt
=> widen AList: Pattern Matching => returns AList (necessary?)
4. cases AMany
e.g. isConcreteElementOf_List
→ \gamma(AMany(ax)) = \gamma(ANil) \union \gamma(ACons(ax, AMany(ax)))
Instead of one case splittet in two cases
case (Nil, AMany())
case (x::xs, AMany())
(avoid union-operator)
Next Steps:
1. union and intersect operators
2. Start with conditions of a lattice
- bottom
- top
- lowest upper bound
- greatest lower bound
- <=
- widen (already started with implementation)
- Definitions: AList
- Definitions: AState
- Examples: Basic Functions
- Examples: Loop
- AList as Set
- Checklist: Operators
- Checklist: Experimental Evaluation
- Meeting Notes: 09.11.21
- Meeting Notes: 15.11.21
- Meeting Notes: 22.11.21
- Meeting Notes: 29.11.21
- Meeting Notes: 14.12.21
- Meeting Notes: 21.12.21
- Meeting-Notes: 11.01.22
- Meeting Notes: 18.02.22
- Meeting Notes: 01.02.22