Talk:Predicate transformer semantics: Difference between revisions

Revision as of 00:03, 23 May 2017

Latest revision as of 17:55, 25 January 2024

(2 intermediate revisions by 2 users not shown)

Line 1:

{{WikiProject Computerbanner Scienceshell|class=C|importance=mid}}

{{WikiProject Computing|software=yes|class=CComputer science|importance=mid}}

{{WikiProject Computing|software=yes|importance=mid}}

}}

A more in-depth discussion of '''if''' and '''do''' is required, as well as nondeterminism. Also, an example of how to use ''predicate transformers'' to derive a non-trivial algorithm might be good, as long as it doesn't conflict with policy. Also, the references section could use some filling out, specifically to the Gries' and Backhous' newer books on the subject. The relationship to [[First-order_logic|predicate calculus]] could also be filled out.

--[[User:Jdinolt|jayinbmore]] 23:58, 31 Jan 2005 (UTC)

Line 63 ⟶ 64:

<p>If we allow an assume statement, the wp operator is not strict:<br>

The weakest precondition of False before the statement <code>assume !A</code> is exactly the formula that satisfies A.</p>

Assume statements are common in the field of software verification<ref name="ZeeKuncak2009">{{cite journal|last1=Zee|first1=Karen|last2=Kuncak|first2=Viktor|last3=Rinard|first3=Martin C.|title=An integrated proof language for imperative programs|journal=ACM SIGPLAN Notices|volume=44|issue=6|year=2009|pages=338|issn=03621340|doi=10.1145/1543135.1542514}}</ref>

Line 72 ⟶ 73:

is typically translated to a start ___location with two outgoing edges

to nodes that represent the entry to the representation of the subprograms C1 and C2.

The edge entering C1 is labeled <code>assume A</code> and the edge entering C2 <code>assume !A</code> respectively.

{{reflist-talk}}