抽象程序设计系统
An Abstract Programming System
摘要：
系统PL允许将程序正确性的抽象证明翻译成各种程序设计语言的程序。满足某些公理的程序设计语言可以是这种转换的目标。系统PL还允许以抽象程序设计语言构造和证明程序的正确性，并允许将这些程序翻译成各种语言的正确程序。抽象程序设计语言具有命令式的编程风格，带有赋值语句和副作用，以允许高效地生成代码。抽象程序可以由人类编写，然后翻译，避免了用不同语言甚至相同语言重复编写相同程序的需要。该系统使用经典逻辑，概念简单，并允许推理使用斯科特-斯特雷奇风格的指称语义的非终止程序。
英文摘要：
The system PL permits the translation of abstract proofs of program correctness into programs in a variety of programming languages. A programming language satisfying certain axioms may be the target of such a translation. The system PL also permits the construction and proof of correctness of programs in an abstract programming language, and permits the translation of these programs into correct programs in a variety of languages. The abstract programming language has an imperative style of programming with assignment statements and side-effects, to allow the efficient generation of code. The abstract programs may be written by humans and then translated, avoiding the need to write the same program repeatedly in different languages or even the same language. This system uses classical logic, is conceptually simple, and permits reasoning about nonterminating programs using Scott-Strachey style denotational semantics.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
