A Logical Treatment of Non-Termination and Program Behaviour

• 作者: Hussein Zedan Martin Ward
• 来源期刊: 软件工程与应用(英文)
• 学科: 医学
• 关键词: FORMAL Methods REFINEMENT Non-Termination Non-Determinism Weakest PRECONDITION Temporal Logic Wide-Spectrum Language
• 年，卷（期）: 2014,（7）
• 页码范围: 555-561
• 页数: 7页
• 分类号: R73

摘要

Can the semantics of a program be represented as a single formula? We show that one formula is insufficient to handle assertions, refinement or slicing, while two formulae are sufficient: A (S) , defining non-termination, and B (S), defining behaviour. Any two formulae A and B will define a corresponding program. Refinement is defined as implication between these formulae.