+++ title = "Semantics of predicates in the abstract" date = "2023-02-04" author = "Yann Herklotz" tags = [] categories = [] backlinks = ["3c3f"] forwardlinks = ["3c3f2"] zettelid = "3c3f1" +++ In the abstract language, which is used to verify the schedules produced by the scheduler, it also has to verify the equivalence of the predicates. However, these predicates have rich semantics, because they include expressions that are taken from the code during the symbolic evaluation. This, however, means that these predicates do not always evaluate to a value, as the context might not contain enough information to evaluate an expression. In addition to that, it's not certain that the expressions are free of undefined behaviour when they are evaluated with an arbitrary context, which would mean that a division that was safe in the input could suddenly become a division by 0.