Hello everyone,<div><br></div><div>I am trying to accomplish the following task, and was wondering if anyone knows of a fitting paper that I can read. I want to write a static analysis tool for a small scheme-like language to catch simple typing errors. The following is a simple example of the type of errors that I would like to detect:</div>
<div><br></div><div>1) let b = (or (pair? x) (string? x))  ;; compute whether x is a pair or a string</div><div>2) assert b   ;; early exit the program if b is false.</div><div>3) result = x * 2 ;; &lt;--- This is a type error that can be found using static analysis.</div>
<div><br></div><div>In words, the pseudocode fragment says:</div><div>1) Let b be a boolean, it indicates whether x is a pair or string.</div><div>2) Assert that b must be true.</div><div>3) Store x times 2 into result. This must be a type error because, for program execution to reach this point, x must either be a pair or a string, otherwise the assertion would have failed. Therefore, since x is either a pair or a string, it is definitely not an integer.</div>
<div><br></div><div>I know the general case is not solvable, but I wish for the tool to detect as many errors as possible. I am currently looking through the abstract interpretation and symbolic execution literature. If anyone knows of a paper that is suitable for my problemd I would be very appreciative.</div>
<div><br></div><div>Thank you very much</div><div>  -Patrick</div>