lemma.js
function pred(x, y) {
return (x+y)===(y+y);
}
var t = new TestCase([[1,1], [2,2], ["1", 1]], pred);
Contract.assert(t);
pred(1,2);
pred.apply(this, [1,2]);
pred.call(this, 1, 2);
pred.bind(this).bind(1).bind(2);
var l = new Lemma([Pos, Neg, typeString], fucntion(x, y) {
return (x+y)===(y+y);
});
Contract.assert(t);
/** Lemma-Dummy
*/
function Lemma(predicate) {
this.predicate = predicate;
}
/**
* Case 1
*/
(function() {
var lemma1 = new Lemma(function(x, y, xs) {
return (!((x<xs) && (y<=x)) || (y<xs));
});
print(lemma1.predicate(1,2,3));
print(lemma1.predicate(2,1,3));
var lemma2 = new Lemma(function(xs, ys) {
return xs.concat(ys).length === xs.length + ys.length;
});
var alpha = ['a', 'b', 'c'],
numeric = [1, 2, 3];
print(lemma2.predicate(alpha, numeric));
var lemma3 = new Lemma(function(xs, ys) {
return (xs.concat(ys).reverse()).toString() == (ys.reverse().concat(xs.reverse())).toString();
});
var alpha = ['a', 'b', 'c'],
numeric = [1, 2, 3];
print(lemma3.predicate(alpha, numeric));
})();
/**
* Case 2
*/
(function() {
/**
* associativity of plus (w.r.t number values)
*/
var predicate1 = function() {
var x=1, y=2;
return (x+y)===(y+x);
}
var lemma1 = new Lemma(predicate1);
/**
* associativity of plus (w.r.t all values)
*/
var predicate2 = function() {
var x="1", y=2;
return (x+y)===(y+x);
}
var lemma2 = new Lemma(predicate2);
})();
/**
* Case 3
*/
(function() {
/**
* a = (pop (push s a))
*/
var lemma1 = new Lemma(function(stack) {
var a = {};
stack.push(a);
return a === stack.pop();
});
print(lemma1.predicate([]));
//lemma1.apply();
//Contract.use(lemma1);
})();