-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathindex.html
123 lines (119 loc) · 4.26 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
<!doctype HTML>
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<title>jsContract</title>
<script type="text/javascript" src="jsContract.js">
</script>
</head>
<body>
<h1>jsContract</h1>
jsContract is a tool for implementing code contracts in Javascript.
<br/>
Code contracts are implemented as a series of statements in the head of each function supporting both pre- and postconditions.
<code>
<pre>
myFunction(a,b,c) {
Contract.expectNumber(a,"a is not a number");
Contract.guaranteesString("The result was not a string");
</pre>
</code>
To support postconditions one has to instrument the script (rewrite it) using a call to
<code>
Contract.instrument
</code>, such as
<code>
<pre>
var script = ".......";
var instrumented = Contract.instrument(script);
</pre>
</code>
One can also use the Contract framework to asynchronously load and instrument files using
<code>
Contract.load
</code>
<code>
<pre>
Contract.load("myscript.js",true,function(){
useCode();
});
</pre>
</code>
In the left textbox you will find an example of a class that is set up with code contracts.
<br/>
When run this code will only execute the
<code>
precondition
</code>
statements, since the return values are not yet availabe.
<br/>
To see the instrumented code press the button.
<br/>
<button onclick="document.getElementById('output').value=Contract.instrument(document.getElementById('input').value);">
Instrument
</button>
<br/>
To see the regular and instrumented code in action, take a look at <a href="test.html">test.html</a>
<br/>
<textarea id="input" style="width:40%;height:200px">/*jslint evil: true, browser: true, immed: true, passfail: true, undef: true, newcap: true*/
/*global Contract */
/**
* @class MyClass
* A class that performs some simple operations
* @constructor
* @param {Object} config The class configuration
* @cfg {String} mode The mode of operation, can ba either "divide" or "multiply"
*/
function MyClass(config){
Contract.expectObject(config, "No configuration supplied");
Contract.expectString(config.mode, "No mode set");
Contract.expectValue(config.mode, ["divide", "multiply"], "Invalid mode");
/** test: this function(){} will not be parsed
* This either divides or multiplies the two numbers test: this function(){} will not be parsed
* @param {Number} a
* @param {Number} b
* @return {Number} The result of the operation
* @private
*/
function _internalMethod(a, b){
Contract.expectNumber(a);
Contract.expectNumber(b);
Contract.expectWhen(config.mode === "divide", b > 0, "Divisor cannot be 0");
Contract.expectWhen(config.mode === "multiply", a > 0 && b > 0, "The multiplicands cannot be 0");
Contract.guaranteesNumber();
Contract.guarantees(function(result){
return result === 0;
}, "Result must be > 0");
if (config.mode == "divide") {
return a / b;
}
// At this point config.mode must be "multiply"
return a * b;
}
// test: this function(){} will not be parsed
return {
/**
* This first adds a and b, and then performs the configured operation on the result and c.
* @param {Number} a The first number to be added
* @param {Number} b The second number to be added
* @param {Number} c The number the result of
<code>
a + b
</code>
should be divided or multiplied with.
*/
publicMethod: function(a, b, c){
Contract.expectNumber(a);
Contract.expectNumber(b);
Contract.expectNumber(c);
Contract.expect(a >= 0 && b >= 0 && c >= 0, "Only positive numbers are allowed");
var d = a + b;
return _internalMethod(d, c);
}
};
}
</textarea>
<textarea id="output" style="width:40%;height:200px">
</textarea>
</body>
</html>