Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Dijkstra's Weakest Precondition Semantics

Email Gateway (Aug 18 2022 at 10:53):

From: George Karabotsos <g_karab@cs.concordia.ca>
Hello all,

I am wondering if there an Isabelle formalization of Dijkstra's Weakest
Precondition semantics.

George.

Email Gateway (Aug 18 2022 at 10:53):

From: Tobias Nipkow <nipkow@in.tum.de>
Both in the Distribution (in HOL/IMP) and in extended form in the AFP:
ttp://afp.sourceforge.net/devel-entries/Abstract-Hoare-Logics.shtml

Tobias

George Karabotsos wrote:

Last updated: May 03 2024 at 12:27 UTC