We aim at a holistic perspective on program logics, including Hoare and incorrectness logics. To this end, we study different classes of properties arising from the generalization of the aforementioned logics. We compare our results with the properties expressible in the language of Kleene algebra with top and tests.
翻译:我们旨在建立程序逻辑的整体视角,涵盖霍尔逻辑与不正确性逻辑。为此,我们研究了从上述逻辑泛化中产生的不同属性类别,并将结果与带顶和测试的克莱尼代数语言所表达的属性进行了比较。