I need a piece of advice from JavaScript guru.
I am developing a formal verification tool for a JavaScript developers (actually for the toy language which is a simplified version of JavaScript, no eval() function included, but still almost whole ECMA Standard).
I need to write a global predicate (or a library of predicates) which will contain some specifications and restrictions for functions from ECMA (hints for a developer).
So developer clicks “show me the hints” and his whole-program code would be automatically checked (via symbolic testing with SMT-solver at the core) for the situations when NaN or undefined behavior can happen… or when function can do something unexpected. It should be more than compiler can suggest, it should be some kind of formal verification.
I am going to write specifications for a JavaScript functions. Specifications, describing expected behavior.
What kind of specifications it can be? What unexpected behavior you faced in your JavaScript code?
Basically I need to inform developer that specific function he is using in his code can lead to undefined behavior in certain circumstances.
Example:
Programmer click “show hints” on next code
const foo = 42; // foo is a number
const result = foo + "1"; //
My instrument will give him a hint:
Warning: foo will be coerced to the **string**! JavaScript coerces foo to a string, so it can be concatenated with the other operand.
Thank you