What you're trying to do is called Formal Verification, and is generally impossible in JS. If, however, you restrict yourself to a subset of the language, it becomes tenable. The usefulness of such an analysis is debatable.
It is certainly used for other languages in areas where safety and correctness is of utmost concern, and development speed can take a back seat (read: medical and space industries foremost). This is a developing field and the methods used are constantly being refined. Some of them are mentioned in the Wiki link.
Since you asked for an example even if this means restricting yourself to a subset, I'll give you a very simple one. You could expand it to use more lax definitions and add more language features to get to a more usable one, but that takes more time than I am ready to commit here. Do note, that I'm not actively working in this field and writing from memory of several courses in university that I took some 6-8 years ago.
Say you restrict your language to only have 1 datatype - 32 bit 2-complement int and only have these operations on it: +
, -
, *
, /
. You have local variables (initialized to 0, unless otherwise specified), that you can assign to via =
. You also have an if
statement that can have <
, >
, =
in it, that is followed by an assignment or return
, and return
to return an int. You do not have any objects, threads, globals or whatevers. For the sake of simplicity, you also do not have method calls (otherwise you'll have to describe how that's done as well). Syntax is vaguely C-like.
Before you run the analyzer, I'll assume that the program actually compiles - no sense doing this otherwise.
Now, you have the method:
0 int max(int a, int b) {
1 if (a > b) return a;
2 if (b > a) return b;
3 return a;
4 }
And you want to check that it returns the maximum of the two ints. So, the post conditions you want to check are (these are usually written in a different language, since this is the input to the checker, not compiler):
res >= a
res >= b
function always returns
Now, the last condition is kinda silly. Since it compiles, the compiler already checked that every method termination ends with a return. And, since there are no loop, jump or call semantics in the language (except return), every operation advances control. But in a slightly more complex language this would be an important and difficult thing to check.
So, if you go the route of Model Checking, you just build a state machine that represents every single state that the program can be in. That's 2^32 * 2^32 * 4
(2 int vars and 4 lines to be on). Obviously that's too many states to hold, so we abstract them by the values the vars can take at the time.
You then start from the end and gather the restrictions on your inputs that got you there.
For ep3
- End Point 3, you return a
. So you set res
= a
. You then step back once, finding all call sites to this return
(in the case of this language it's always just 1 step back).
You find that you can only get to this return
if the previous if
was false. Hence, now you have a restriction - NOT b > a
. You then step back another time and get the restriction NOT a > b
. You've now reached the beginning of your method and you have a result: a
and restrictions on input: NOT b > a AND NOT a > b
.
Then you use formal logic rules defined on int
that describe all various restrictions that you can have on variables to show that the restriction you have implies the conditions you want.
Rinse and repeat for the other 2 exit points.
Now you've proved that if the method returns, it returns the max value. The 3rd condition that I've skipped proved that it always returns. Hence the program is correct in the semantics given.
A less silly example would be:
0 int abs(int a) {
1 if (a < 0) return -1 * a;
2 return a;
3 }
With the post-condition of:
res >= 0
res == a OR res == -a
ep2
is very simple - you get res == a AND NOT a < 0
, which clearly satisfies our conditions.
ep1
is tricky, since there are several operations there. The final operation is a * -1
. This is typically done via a dedicated circuit, but we are essentially interested in everything that it can do to a number expressed in logical rules. For summation this would be something like:
a, b -> (res = a + b AND a + b <= MAX_INT AND a + b >= MIN_INT)
OR (res = a + b - INT_RANGE AND a + b >= MAX_INT)
OR (res = a + b + INT_RANGE AND a + b <= MIN_INT)
I'll note again, that since the logic specification is written in a different language, it uses a datatype that is guaranteed to not overflow on these ops.
You can imagine the same thing done for multiplication, explaining the exact pre- and post-conditions of multiplication for overflow.
So now we return to the method at hand and get the following result of the post-conditions:
a < 0 AND (
(res = -a AND -a <= MAX_INT) //No overflow
OR (res = -a mod INT_RANGE AND -a > MAX_INT) //positive overflow
OR (res = -a mod INT_RANGE AND -a < MIN_INT) //negative overflow
)
Since this is written in a language with guaranteed no overflows, you can use rules like a < 0 => -a >= 0
. Do exactly that and you get:
(res = -a AND -a >= 0 AND -a <= MAX_INT)
OR (res = -a mod INT_RANGE AND -a >= 0 AND -a > MAX_INT)
OR (res = -a mod INT_RANGE AND -a >= 0 AND -a < MIN_INT)
You then eliminate the last expression - it's impossible. You also eliminate the first expression - the post-conditions obviously follow from it.
You're left with the possibility of res = -a mod INT_RANGE AND -a > MAX_INT
. The last part of this morphs into a < -MAX_INT
.
The analyzer will then, most likely, say - it can't prove correctness when input is below -MAX_INT. This is the general case of analyzers - most of the time they will not tell you there's a mistake, but rather say they can't prove there isn't one.
You can see how this is very tedious, and adding even simple OPs is difficult - you have to completely describe its operation and every possible outcome in your logic of choice. Adding language features will usually give an exponential explosion in complexity and allowing a fully Turing-complete language will make the general case impossible.
eval
exists, and other reasons. Same for Java, due to reflection and runtime loading of classes. If, however, you restrict yourself to a well-behaved subset of those languages, the methods mentioned in the Wiki will work.