Meeting Notes: 14.12.21

• Examples loop:
  • put assertions in the comments, so it's more obvious what test is doing
  • n and xs are abstract values: n is not a concrete value like 0, it's of type AInt like [0,0]
  • doesn't have to be implemented with a while statement, it's enough to have e.g. 3 runs
  • 2 or 3 examples are enough, need to be well commented
• Research:
  • Do some research on how to translate concrete values into abstract values
  • Pattern Matching
    • Concretization: outer part
    • Patter Matching: in the methods
  • assert: with Boolean or ABool
• Method justAList (returns the value of type AList of a AOption[AList] statement) should only work for ASome (and the AMany - Part which is definitely not ANil)
• implement === for Intervals, AList, ABool and AOption
• implement !== for ABool
• implement equals(xs: AList, ys: AList) : ABool
• new Package for AList as Set
  • traits are the same
  • methods and operations take as parameters inputs like Set[AList] and also returns statements like Set[AList]
  • implement aTail, aHead and isNil
• Start preparing slides for the presentation (Motivation, Goals, Preliminary work, Example, Timeline)
• Long-term goal:
  • for every implemented program-operation like head, ==, tail, + , && exists a abstract version
    • head : List[Int] -> Option [Int]
    • aHead :Set[AList[AInt]] -> Set[AOption[AInt]]
  • for every program-construct like while exists a abstract version
    • while(t) {b}: State -> State
    • A[while(t) {b}]: Set[AState] -> Set[AState]