变量符号静态分析的伪代码算法——检查每个操作的符号

Question

我想对变量（仅限整数）进行静态符号分析。

示例：我有两个变量的可能符号和操作

一个正 + 一个正 = 一个正 [Pos] + [Pos] -> [Pos]

正数或零 + 正数 = 正数 [Pos; Zero] + [Pos] -> [Pos]

A 正或零或负 * 零 = 零 [Pos; Zero; Neg] * [Zero] -> [Zero]

等等...

我的变量符号被编码为列表/数组。

正变量或零变量将被编码为[Pos; Zero] 负变量将被编码为 [Neg] 正变量、负变量或零变量将被编码为 [Pos;否定;零]顺序无关紧要[Pos;零] 与 [零;位置]

我需要在 OCAML 中执行此操作，但您可以使用任何语言/伪代码提供帮助。

这是我的想法：

let sign_operation (op:op) (l_expr: sign list) (r_expr: sign list): sign list = 
  match op with 
  | Add -> (match l_expr, r_expr with 
      | [Pos], [Pos] -> [Pos]
      | [Pos], [Zero] -> [Pos]
      | [Zero], [Pos] -> [Pos]
      | [Pos], [Neg] -> [Neg;Zero;Pos]
      | [Neg], [Pos] -> [Neg;Zero;Pos]
      | [Neg], [Zero] -> [Neg]
      | [Zero], [Neg] -> [Neg]
      | [Neg], [Neg] -> [Neg]
      | [Zero], [Zero] -> [Zero]
      | _ -> failwith "no")

  | Sub -> (match l_expr, r_expr with 
      | [Pos], [Pos] -> [Neg;Zero;Pos]
      | [Pos], [Zero] -> [Pos]
      | [Zero], [Pos] -> [Neg]
      | [Pos], [Neg] -> [Pos]
      | [Neg], [Pos] -> [Neg]
      | [Neg], [Zero] -> [Neg]
      | [Zero], [Neg] -> [Pos]
      | [Neg], [Neg] -> [Neg;Zero;Pos]
      | [Zero], [Zero] -> [Zero]
      | _ -> failwith "no")

  | Mul -> (match l_expr, r_expr with 
      | [Pos], [Pos] -> [Pos]
      | [Pos], [Zero] -> [Zero]
      | [Zero], [Pos] -> [Zero]
      | [Pos], [Neg] -> [Neg]
      | [Neg], [Pos] -> [Neg]
      | [Neg], [Zero] -> [Zero]
      | [Zero], [Neg] -> [Zero]
      | [Neg], [Neg] -> [Pos]
      | [Zero], [Zero] -> [Zero]
      | [Neg;Zero;Pos], [Zero] -> [Zero]
      | [Zero], [Neg;Zero;Pos] -> [Zero]
      | _ , [Zero] -> [Zero]
      | [Zero] , _ -> [Zero]
      | _ -> failwith "no")

  | Div -> (match l_expr, r_expr with 
      | [Pos], [Pos] -> [Pos]
      | [Pos], [Zero] -> [Error]
      | [Zero], [Pos] -> [Zero]
      | [Pos], [Neg] -> [Neg]
      | [Neg], [Pos] -> [Neg]
      | [Neg], [Zero] -> [Error]
      | [Zero], [Neg] -> [Zero]
      | [Neg], [Neg] -> [Pos]
      | [Zero], [Zero] -> [Error]
      | [Neg;Zero;Pos], [Zero] -> [Error]
      | [Zero], [Neg;Zero;Pos] -> [Zero]
      | _ -> [Error])

  | Mod -> (match l_expr, r_expr with 
      | [Pos], [Pos] -> [Pos]
      | [Pos], [Zero] -> [Error]
      | [Zero], [Pos] -> [Zero]
      | [Pos], [Neg] -> [Error]
      | [Neg], [Pos] -> [Error]
      | [Neg], [Zero] -> [Error]
      | [Zero], [Neg] -> [Error]
      | [Neg], [Neg] -> [Error]
      | [Zero], [Zero] -> [Error]
      | _ -> [Error])

这不适用于任何具有两个或更多可能符号的变量。

如果我有一个变量[Pos;零; Neg] 负 [Pos;零]，这不会在我的模式中匹配。在每个可能的顺序中尝试每个可能的排列会太长。

你能推荐一个更好的方法吗？

抱歉，如果我不能很好地理解自己，请随时提出任何问题，谢谢！

Answer 1

在你的问题中，你写

A Positive or Zero + A positive = A Positive [Pos; Zero] + [Pos] -> [Pos]

你怎么知道的？你上过一所专门教你给某物加一个正数或零数会得到什么的学校吗？当然不是。您将其分解为更简单的案例，推理如下：

第一个数字可能是正数。在那种情况下，我知道 Pos+Pos = Pos
第一个数字可能是零。在那种情况下，我知道 Zero+Pos = Pos.
因此，在第一个数字可能包含的所有值中，结果是 Pos 或 Pos。
当然，我们可以将其简化为始终为 Pos。

写一个程序，用同样的方式推理。不要一次查看一对符号列表，而是为每个操作编写一个函数，该函数只处理每个操作数的一个符号，从而产生可能结果的列表。对输入列表表示的每对可能的符号调用该函数，然后合并结果。

例如

signOp Add x y = case (x, y) of
  (Zero, r) -> [r]
  (l, Zero) -> [l]
  _ | x == y -> [x]
    | otherwise -> [Pos, Zero, Neg]

Answer 2

处理此问题的实用方法如下：

let compare (s0 : sign) (s1 : sign) : int =
   match (s0,s1) with
   | (x,y) when x = y -> 0
   | (Neg, _) | (_, Pos) -> 1
   | (Pos,_) | (_,Neg) -> -1

(* flatten and remove duplicates *)
let join ( xs : (sign list) list) : (sign list) = 
   List.sort_uniq compare (List.flatten xs)

let add (s0 : sign) (s1 : sign) : sign list = 
   match (s0,s1) with
   | (x,y) when x = y -> [x]
   | (Pos, Zero) | (Zero, Pos) -> [Pos]
   | (Neg, Zero) | (Zero, Neg) -> [Neg]
   | (Pos,Neg) | (Neg, Pos) -> [Pos;Neg;Zero]

let add_list (sl : sign list) (s : sign) : sign list =
   join (List.map (add s) sl)
  
let add_abstract (sl0 : sign list) (sl1 : sign list) : sign list =
   join (List.map (add_list sl0) sl1)

对于减法和除法等非交换运算，您可能需要更加小心。

如果您了解 monad，OCaml 的做法如下：

(* "let*" is "bind" or ">>=" in Haskell *)
let (let*) (sl : sign list) (f : sign -> sign list) : sign list =
  join (List.map f sl)

let add_list (sl : sign list) (s : sign) : sign list =
  let* s0 = sl in
  (add s s0)

let add_abstract (sl0 : sign list) (sl1 : sign list) : sign list =
  let* s0 = sl0 in
  let* s1 = sl1 in
  (add s0 s1)

变量符号静态分析的伪代码算法——检查每个操作的符号

Pseudocode algorithm for variables' signs static analysis - Check the sign of each operation

algorithm

haskell

ocaml

static-analysis