我有一种语言需要确定我的流程控制语句谓词是重言式还是矛盾

Question

您好，我正在与我的项目组一起研究领域特定语言。如果 if(predicate) 或 while(predicate) 中的谓词始终为真或始终为假，我们想向语言用户报告。在该语言上实现的逻辑运算符是 AND、OR、NEGATION 以及比较运算符 <、>、>=、<=、!=、=(equal)。

我自然只想检查带有文字符号的谓词，例如false、true、数字和字符串。评估表达式的值符号没有问题。

所有这些都是可能的吗？它们是否是我可以查看的现有信息，甚至是一些代码？

Answer 1

如果控制流没有循环（并且没有 gotos 和 recusion；任何可以用来模拟无限循环的东西）这是可能的。您可以使用 SMT 求解器来求解几乎任意的公式，并告诉您某个布尔表达式是否始终为真或假。该 SMT 求解器的运行时间可能不切实际。一些 SMT 求解器也不完整。他们有时会回答 "unknown"。看看Z3。它是免费的，而且质量和性能都非常高。

如果涉及任意控制流（如果这是一种图灵完备的语言），那么停机问题表明您通常无法解决此问题。您将不得不采用启发式方法。

我认为你的方法不应该是语言设计的一部分。使其成为允许有时回答 "I don't know".

的静态分析工具

Answer 2

如果您将公式限制为谓词叶上的布尔逻辑（例如，您在 "ground literals" 处处理关系比较），则可以通过应用 Wang 的推理规则来验证公式是否为重言式，这里捕获在代数规范中，其中公理可以被视为从左到右的重写规则：

WANG =
{   sort Boolean;

    true, false: Boolean;

    Boolean generated by true, false;

    not: Boolean ® Boolean;
    and, or: Boolean --> Boolean ® Boolean
               associative commutative;
    implies, equivalent: Boolean --> Boolean ® Boolean;

    axioms
    -- 3 simplification rules for not
        «not1»  not(true) = false;
        «not2»  not(false) = true;
        «not3»  not(not(x)) = x;
    -- definition of 'implies'
        «impl»  implies(x,y) = or(not(x),y);
    -- definition of 'and'
        «and»  and(x,y) = not(or(not(x),not(y)));
    -- definition of 'equivalent'
        «eq»    equivalent(x,y) = and(implies(x,y),implies(y,x));
    -- simplification rules for 'or'
        «or01»  or(true,x) = true;
        «or02»  or(false,x) = x;
        «or03»  or(x,not(x)) = true;
        «or04»  or(x,or(not(x),y)) = true;
        «or05»  or(x,x) = x;
        «or06»  or(x,or(x,y)) = or(x,y);
        «or07»  or(not(or(x,y)),x) = or(x,not(y));
        «or08»  or(not(or(x,y)),or(x,z)) = or(x,or(not(y),z));
        «or09»  or(not(or(x,y)),not(x)) = not(x);
        «or10»  or(not(or(x,y)),or(not(x),z)) = or(not(x),z);
        «or11»  or(not(or(not(x),y)),x) = x;
        «or12»  or(not(or(not(x),y)),or(x,z)) = or(x,z);
        «or13»  or(not(or(not(x),y)),not(or(x,y))) = not(y);
        «or14»  or(not(or(not(x),y)),or(not(or(x,y)),z)) = or(not(y),z);
 endaxioms;
}

这些重写规则的美妙之处在于您可以按任何顺序将它们应用于布尔方程。最终，不再适用任何规则。在这一点上，你的公式要么是 TRUE（重言式），要么是 FALSE（反重言式），要么是其他东西（既不是 TRUE 也不是 FALSE）。

（此特定规则集直接由 DMS Software Reengineering Toolkit 应用。您可以通过为布尔表达式构建（抽象）语法树来实现自己的 "rewriter"，然后实现所有这些规则相对简单遍历树寻找它们可能应用的位置的过程，并在找到这样的位置时简单地应用它们。这实际上非常简单。）。

我有一种语言需要确定我的流程控制语句谓词是重言式还是矛盾

I have a language where I need to determine if my flow control statement predicates are tautologies or contradictions

compiler-construction

compiler-errors

boolean-expression