Generic Commands - A Tool for Partial Correctness Formalisms
Generic Commands - A Tool for Partial Correctness Formalisms
复制标题
通用命令 - 部分正确形式主义的工具
DOI：
10.1093/comjnl/20.2.151
复制
发表时间：
1977
期刊：
影响因子：
--
通讯作者：
J. Schwarz
中科院分区：
文献类型：
--
作者：
J. Schwarz
给出了基于 P{S}Q 形式的部分正确性断言的逻辑形式主义的语义框架。P{S}Q 断言 ifP 在执行 SthenQ 之前保持。介绍了通用命令。通用命令{P=≥Q}在某种意义上是具有前置条件P和后置条件Q的最少指定命令。为通用命令给出了证明规则和无效语义。递归过程的证明规则是使用通用命令给出的。
A semantic framework for logical formalisms based on partial correctness assertions of the formP{S}Qis given.P{S}Qasserts that ifPholds before execution ofSthenQholds after. Generic commands are introduced. The generic command{P=≥Q}is in a sense the least specified command with preconditionPand postconditionQ. Proof rules and a noneffective semantics are given for generic commands. A proof rule for recursive procedures is given using generic commands.