11## JavaScript Program Verification
22
3- You can verify a JavaScript program by using the semantics and the K verifier.
4-
5- All you need to do is to write a specification and run ` krun ` with ` --prove ` option:
3+ The JavaScript program verifier combines the K verification infrastructure with the JavaScript semantics.
4+ The verification is enabled by the ` --prove ` option of the ` krun ` command:
65```
76$ krun --prove <specification.k> <program.js>
87```
9- The specification ` <specification.k> ` essentially describes a pre-/post-condition ,
8+ The specification ` <specification.k> ` essentially describes a set of pre-/post-conditions ,
109and it should be given as a reachability rule written in K.
1110
12- You can quickly run all of the verification examples using the [ Makefile ] ( Makefile ) :
11+ Use the [ Makefile ] ( Makefile ) to quickly run all of the verification examples:
1312```
1413$ make
1514```
16-
17- We provide the verification results, [ verification.out] ( verification.out ) .
18- For each program, the verifier simply outputs the following triple when it succeeds in verifying the program:
19- ```
20- true
21- []
22- true
23- ```
24- Note that the verifier will simply crash or not terminate when the program is not correct. We will improve usability of the verifier in the future.
15+ The output of the ``` make ``` command is available in [ verification.out] ( verification.out ) .
16+ For each program, the verifier simply outputs ``` true ``` when it succeeds in verifying the program.
17+ Note that the verifier may crash or fail to terminate when the program is not correct.
18+ We will improve usability of the verifier in the future.
2519
2620
2721### List of Programs and Specifications
@@ -40,7 +34,6 @@ We have the following example programs and specifications to be verified:
4034| AVL delete | [ avl/avl.js: delete ] ( avl/avl.js#L120 ) | [ avl/avl_delete_spec.k] ( avl/avl_delete_spec.k ) |
4135
4236
43-
4437### Specifications
4538
4639The specifications are given as reachability rules using the K syntax and are
5548 (.Bag => ?_:Bag)
5649 ...</envs>
5750 <objs>...
58- (string_htree (O1)(T1:StringTree) => string_htree (?O2)(?T2:StringTree))
51+ (htree (O1)(T1:StringTree) => htree (?O2)(?T2:StringTree))
5952 OBJS:Bag
6053 (.Bag => ?_:Bag)
6154 ...</objs>
6861 =>
6962 ?O2:NullableObject
7063 ...</k>
71- requires string_avl (T1) andBool string_tree_height (T1) <Int (4294967296 -Int 1)
72- ensures string_avl (?T2) andBool string_tree_keys (?T2) ==K { V } U string_tree_keys (T1)
73- andBool string_tree_height (T1) <=Int string_tree_height (?T2)
74- andBool string_tree_height (?T2) <=Int string_tree_height (T1) +Int 1
64+ requires avl (T1) andBool tree_height (T1) <Int (4294967296 -Int 1)
65+ ensures avl (?T2) andBool tree_keys (?T2) ==K { V } U tree_keys (T1)
66+ andBool tree_height (T1) <=Int tree_height (?T2)
67+ andBool tree_height (?T2) <=Int tree_height (T1) +Int 1
7568```
7669
7770While the rule is fairly verbose (due to operating on the configuration used to
@@ -85,35 +78,34 @@ Specifically
8578 * the parts that captures general JavaScript behavior; e.g. the line
8679 ` (.Bag => ?_:Bag) `
8780 in the ` <objs> ` cell that says that after a function call there may be some
88- dead objects left over, since the semantics does not garbage collect (` ?\ _ ` is a
81+ dead objects left over, since the semantics does not garbage collect (` ?_ ` is a
8982 existentially quantified anonymous variable)
90- * the internal reference to the ` insert ` function, ` @o(19) ` , will be automatically generated.
83+ * the internal reference to the ` insert ` function, ` @o(19) ` (which can be automatically generated) .
9184
9285The parts of this rule specific to the avl insert routine are
9386 * the ` <k> ` cell, which says that the call to insert takes a string ` V ` and an
9487 object reference ` O1 ` and returns another object reference ` ?O2 `
9588 * the line
96- ` (string_htree (O1)(T1:StringTree) => string_htree (?O2)(?T2:StringTree)) `
89+ ` (htree (O1)(T1:StringTree) => htree (?O2)(?T2:StringTree)) `
9790 in the ` <objs> ` cell which says that before the call to insert, there is a tree
9891 rooted at ` O1 ` which represent the algebraic tree ` T1 ` in the heap, and after the
9992 call there is another tree rooted at ` ?O2 ` which represents the tree ` ?T2 `
100- * the requires clause, which i) states that ` T1 ` is an avl, ii) bounds the height
101- of ` T1 ` to ensure there is no precision loss when computing the height of ` ?T2 `
102- (the tree after the insertion), and iii) states that insert has not been
103- redefined between the global declaration and the call site
104- * the ensures clause which states that i) ` ?T2 ` is an avl, ii) they keys of ` ?T2 `
93+ * the requires clause, which i) states that ` T1 ` is an avl, and ii) bounds the
94+ height of ` T1 ` to ensure there is no precision loss when computing the height of
95+ ` ?T2 ` (the tree after the insertion)
96+ * the ensures clause, which states that i) ` ?T2 ` is an avl, ii) the keys of ` ?T2 `
10597 are the union of the keys of ` T1 ` and ` { V } ` , and iii) the height of ` ?T2 `
10698 increases by at most one
10799
108100With that in mind, we could generate the rule above from a more compact
109101annotation
110102```
111103function insert(v, t)
112- //@requires string_htree (t)(T1) /\ string_avl (T1)
113- /\ string_tree_height (T1) < 4294967295
114- //@ensures string_htree (t)(?T2) /\ string_avl (?T2)
115- /\ string_tree_keys (?T2) == { V } U string_tree_keys (T1)
116- /\ | string_tree_height (?T2) - string_tree_height (T1) | < 1
104+ //@requires htree (t)(T1) /\ avl (T1)
105+ /\ tree_height (T1) < 4294967295
106+ //@ensures htree (t)(?T2) /\ avl (?T2)
107+ /\ tree_keys (?T2) == { V } U tree_keys (T1)
108+ /\ | tree_height (?T2) - tree_height (T1) | < 1
117109```
118110
119111We did not implement this transformation yet. However a similar transformation
@@ -139,6 +131,7 @@ module JS-VERIFIER
139131endmodule
140132```
141133
134+
142135### Directory Structure
143136
144137 * [ patterns] ( patterns ) - definitions of the abstractions used in the specifications (list, tree, etc) given in K syntax
0 commit comments