Аннотация:
Алгебры Клини с тестами (KAT) являются фундаментальным эквациональным фреймворком для рассуждений про программы. Они нашли свое применение в рассуждениях о трансформациях программ, оптимизациях компиляторов и т.д. В тоже время одной из основополагающих логик для доказательств корректности программ является логика Хоара (HL). В первой половине доклада мы посмотрим на классический результат, связывающий HL и KAT, описанный в работе Козена 2000 г. (https://www.cs.cornell.edu/~kozen/Papers/Hoare.pdf), а именно, как можно задавать семантику HL в терминах KAT. Кроме того, в последнее время все большую популярность приобретает дуальная к HL логика некорректности (IL). Во второй половине доклада мы обсудим последние результаты о связи KAT и IL (Zhang et al. 2021, https://arxiv.org/pdf/2108.07707.pdf). В частности, разберем, почему нельзя задать семантику IL в KAT, и что надо добавить к KAT, чтобы все получилось.
Обратная связь: