' + _('Hide Search Matches') + '
') - .appendTo($('#searchbox')); - } - }, - - /** - * init the domain index toggle buttons - */ - initIndexTable : function() { - var togglers = $('img.toggler').click(function() { - var src = $(this).attr('src'); - var idnum = $(this).attr('id').substr(7); - $('tr.cg-' + idnum).toggle(); - if (src.substr(-9) === 'minus.png') - $(this).attr('src', src.substr(0, src.length-9) + 'plus.png'); - else - $(this).attr('src', src.substr(0, src.length-8) + 'minus.png'); - }).css('display', ''); - if (DOCUMENTATION_OPTIONS.COLLAPSE_INDEX) { - togglers.click(); - } - }, + }; - /** - * helper function to hide the search marks again - */ - hideSearchWords : function() { - $('#searchbox .highlight-link').fadeOut(300); - $('span.highlighted').removeClass('highlighted'); + const togglerElements = document.querySelectorAll("img.toggler"); + togglerElements.forEach((el) => + el.addEventListener("click", (event) => toggler(event.currentTarget)) + ); + togglerElements.forEach((el) => (el.style.display = "")); + if (DOCUMENTATION_OPTIONS.COLLAPSE_INDEX) togglerElements.forEach(toggler); }, - /** - * make the url absolute - */ - makeURL : function(relativeURL) { - return DOCUMENTATION_OPTIONS.URL_ROOT + '/' + relativeURL; - }, - - /** - * get the current relative url - */ - getCurrentURL : function() { - var path = document.location.pathname; - var parts = path.split(/\//); - $.each(DOCUMENTATION_OPTIONS.URL_ROOT.split(/\//), function() { - if (this === '..') - parts.pop(); - }); - var url = parts.join('/'); - return path.substring(url.lastIndexOf('/') + 1, path.length - 1); - }, - - initOnKeyListeners: function() { - $(document).keydown(function(event) { - var activeElementType = document.activeElement.tagName; - // don't navigate when in search box, textarea, dropdown or button - if (activeElementType !== 'TEXTAREA' && activeElementType !== 'INPUT' && activeElementType !== 'SELECT' - && activeElementType !== 'BUTTON' && !event.altKey && !event.ctrlKey && !event.metaKey - && !event.shiftKey) { - switch (event.keyCode) { - case 37: // left - var prevHref = $('link[rel="prev"]').prop('href'); - if (prevHref) { - window.location.href = prevHref; - return false; + initOnKeyListeners: () => { + // only install a listener if it is really needed + if ( + !DOCUMENTATION_OPTIONS.NAVIGATION_WITH_KEYS && + !DOCUMENTATION_OPTIONS.ENABLE_SEARCH_SHORTCUTS + ) + return; + + document.addEventListener("keydown", (event) => { + // bail for input elements + if (BLACKLISTED_KEY_CONTROL_ELEMENTS.has(document.activeElement.tagName)) return; + // bail with special keys + if (event.altKey || event.ctrlKey || event.metaKey) return; + + if (!event.shiftKey) { + switch (event.key) { + case "ArrowLeft": + if (!DOCUMENTATION_OPTIONS.NAVIGATION_WITH_KEYS) break; + + const prevLink = document.querySelector('link[rel="prev"]'); + if (prevLink && prevLink.href) { + window.location.href = prevLink.href; + event.preventDefault(); } break; - case 39: // right - var nextHref = $('link[rel="next"]').prop('href'); - if (nextHref) { - window.location.href = nextHref; - return false; + case "ArrowRight": + if (!DOCUMENTATION_OPTIONS.NAVIGATION_WITH_KEYS) break; + + const nextLink = document.querySelector('link[rel="next"]'); + if (nextLink && nextLink.href) { + window.location.href = nextLink.href; + event.preventDefault(); } break; } } + + // some keyboard layouts may need Shift to get / + switch (event.key) { + case "/": + if (!DOCUMENTATION_OPTIONS.ENABLE_SEARCH_SHORTCUTS) break; + Documentation.focusSearchBar(); + event.preventDefault(); + } }); - } + }, }; // quick alias for translations -_ = Documentation.gettext; +const _ = Documentation.gettext; -$(document).ready(function() { - Documentation.init(); -}); +_ready(Documentation.init); diff --git a/_static/documentation_options.js b/_static/documentation_options.js index 16442b3a64..1df48e1a21 100644 --- a/_static/documentation_options.js +++ b/_static/documentation_options.js @@ -1,12 +1,13 @@ -var DOCUMENTATION_OPTIONS = { - URL_ROOT: document.getElementById("documentation_options").getAttribute('data-url_root'), +const DOCUMENTATION_OPTIONS = { VERSION: '0.9.1', - LANGUAGE: 'None', + LANGUAGE: 'en', COLLAPSE_INDEX: false, BUILDER: 'html', FILE_SUFFIX: '.html', LINK_SUFFIX: '.html', HAS_SOURCE: true, SOURCELINK_SUFFIX: '.txt', - NAVIGATION_WITH_KEYS: false + NAVIGATION_WITH_KEYS: false, + SHOW_SEARCH_SUMMARY: true, + ENABLE_SEARCH_SHORTCUTS: true, }; \ No newline at end of file diff --git a/_static/invalid/AbstractRefinementMap.scala b/_static/invalid/AbstractRefinementMap.scala index d11db628b1..45bae7c9b2 100644 --- a/_static/invalid/AbstractRefinementMap.scala +++ b/_static/invalid/AbstractRefinementMap.scala @@ -12,7 +12,7 @@ object AbstractRefinementMap { def apply(x: A): B = { require(f.pre(x)) f(x) - } ensuring(ens) + }.ensuring(ens) } def map[A, B](l: List[A], f: A ~> B): List[B] = { @@ -21,6 +21,6 @@ object AbstractRefinementMap { case Cons(x, xs) => Cons[B](f(x), map(xs, f)) case Nil() => Nil[B]() } - } ensuring { res => forall((x: B) => res.contains(x) ==> f.ens(x)) } + }.ensuring { res => forall((x: B) => res.contains(x) ==> f.ens(x)) } } diff --git a/_static/invalid/BadConcRope.scala b/_static/invalid/BadConcRope.scala index dfff26ec5b..e050ac93bc 100644 --- a/_static/invalid/BadConcRope.scala +++ b/_static/invalid/BadConcRope.scala @@ -84,7 +84,7 @@ object BadConcRope { case Append(l, r) => 1 + max(l.level, r.level) }): BigInt - } ensuring (_ >= 0) + }.ensuring(_ >= 0) val size: BigInt = { (this match { @@ -95,7 +95,7 @@ object BadConcRope { case Append(l, r) => l.size + r.size }): BigInt - } ensuring (_ >= 0) + }.ensuring(_ >= 0) def toList: List[T] = { this match { @@ -106,7 +106,7 @@ object BadConcRope { case Append(l, r) => l.toList ++ r.toList } - } ensuring (res => res.size == this.size) + }.ensuring(res => res.size == this.size) } case class Empty[T]() extends Conc[T] @@ -125,7 +125,7 @@ object BadConcRope { if (i < l.size) lookup(l, i) else lookup(r, i - l.size) } - } ensuring (res => instAppendIndexAxiom(xs, i) && // an auxiliary axiom instantiation that required for the proof + }.ensuring(res => instAppendIndexAxiom(xs, i) && // an auxiliary axiom instantiation that required for the proof res == xs.toList(i)) // correctness @@ -150,7 +150,7 @@ object BadConcRope { case Append(l, r) => Append(update(l, i, y), r) } - } ensuring (res => instAppendUpdateAxiom(xs, i, y) && // an auxiliary axiom instantiation + }.ensuring(res => instAppendUpdateAxiom(xs, i, y) && // an auxiliary axiom instantiation res.level == xs.level && // heights of the input and output trees are equal res.valid && // tree invariants are preserved res.toList == xs.toList.updated(i, y) && // correctness @@ -188,7 +188,7 @@ object BadConcRope { case _ => concatNonEmpty(xs, ys) } - } ensuring (res => res.valid && // tree invariants + }.ensuring(res => res.valid && // tree invariants res.level <= max(xs.level, ys.level) + 1 && // height invariants res.level >= max(xs.level, ys.level) && (res.toList == xs.toList ++ ys.toList) && // correctness @@ -239,7 +239,7 @@ object BadConcRope { } } } - } ensuring (res => + }.ensuring(res => appendAssocInst(xs, ys) && // instantiation of an axiom res.level <= max(xs.level, ys.level) + 1 && // height invariants res.level >= max(xs.level, ys.level) && @@ -291,7 +291,7 @@ object BadConcRope { case CC(l, r) => concatNonEmpty(l, insert(r, i - l.size, y)) } - } ensuring (res => insertAppendAxiomInst(xs, i, y) && // instantiation of an axiom + }.ensuring(res => insertAppendAxiomInst(xs, i, y) && // instantiation of an axiom res.valid && res.isNormalized && // tree invariants res.level - xs.level <= 1 && res.level >= xs.level && // height of the output tree is at most 1 greater than that of the input tree res.toList == insertAtIndex(xs.toList, i, y) // correctness @@ -356,7 +356,7 @@ object BadConcRope { (l, r) } } - } ensuring (res => instSplitAxiom(xs, n) && // instantiation of an axiom + }.ensuring(res => instSplitAxiom(xs, n) && // instantiation of an axiom res._1.valid && res._2.valid && // tree invariants are preserved res._1.isNormalized && res._2.isNormalized && xs.level >= res._1.level && xs.level >= res._2.level && // height bounds of the resulting tree @@ -382,7 +382,7 @@ object BadConcRope { case Empty() => ys case Single(_) => CC(xs, ys) } - } ensuring (res => res.valid && //conctree invariants + }.ensuring(res => res.valid && //conctree invariants res.toList == xs.toList ++ Cons(x, Nil[T]()) && //correctness res.level <= xs.level + 1 ) @@ -408,7 +408,7 @@ object BadConcRope { Append(l, zs) } } - } ensuring (res => appendAssocInst2(xs, ys) && + }.ensuring(res => appendAssocInst2(xs, ys) && res.valid && //conc tree invariants res.toList == xs.toList ++ ys.toList && //correctness invariants res.level <= xs.level + 1 ) @@ -428,7 +428,7 @@ object BadConcRope { case Append(l, r) => numTrees(l) + 1 case _ => BigInt(1) } - } ensuring (res => res >= 0) + }.ensuring(res => res >= 0) def normalize[T](t: Conc[T]): Conc[T] = { require(t.valid) @@ -439,7 +439,7 @@ object BadConcRope { concatNormalized(l, r) case _ => t } - } ensuring (res => res.valid && + }.ensuring(res => res.valid && res.isNormalized && res.toList == t.toList && //correctness res.size == t.size && res.level <= t.level //normalize preserves level and size @@ -454,7 +454,7 @@ object BadConcRope { case l => concatNormalized(l, nr) } - } ensuring (res => + }.ensuring(res => appendAssocInst2(xs, ys) && //some lemma instantiations res.valid && res.isNormalized && diff --git a/_static/invalid/BraunTree.scala b/_static/invalid/BraunTree.scala index 7733dcd0ec..a2986c5d42 100644 --- a/_static/invalid/BraunTree.scala +++ b/_static/invalid/BraunTree.scala @@ -14,7 +14,7 @@ object BraunTree { Node(value, insert(left, x), right) case Leaf() => Node(x, Leaf(), Leaf()) } - } ensuring { res => isBraun(res) } + }.ensuring { res => isBraun(res) } def height(tree: Tree): Int = { tree match { diff --git a/_static/invalid/Choose.scala b/_static/invalid/Choose.scala index 7508725001..8bb0bb0726 100644 --- a/_static/invalid/Choose.scala +++ b/_static/invalid/Choose.scala @@ -11,7 +11,7 @@ object Choose1 { def size(l: List) : BigInt = (l match { case Nil() => BigInt(0) case Cons(_, t) => 1 + size(t) - }) ensuring(res => res >= 0) + }).ensuring(res => res >= 0) def content(l: List) : Set[Int] = l match { case Nil() => Set.empty[Int] @@ -26,7 +26,7 @@ object Choose1 { } else { choose[List] { (res: List) => size(res) == i-1 } } - } ensuring ( size(_) == i ) + }.ensuring( size(_) == i ) def listOfSize2(i: BigInt): List = { @@ -37,5 +37,5 @@ object Choose1 { } else { Nil() } - } ensuring ( size(_) == i ) + }.ensuring( size(_) == i ) } diff --git a/_static/invalid/InsertionSort.scala b/_static/invalid/InsertionSort.scala index 98aa2325d1..d54d68943e 100644 --- a/_static/invalid/InsertionSort.scala +++ b/_static/invalid/InsertionSort.scala @@ -15,7 +15,7 @@ object InsertionSort { def size(l : List) : BigInt = (l match { case Nil() => BigInt(0) case Cons(_, xs) => 1 + size(xs) - }) ensuring(_ >= 0) + }).ensuring(_ >= 0) def contents(l: List): Set[Int] = l match { case Nil() => Set.empty @@ -36,7 +36,7 @@ object InsertionSort { case Nil() => Cons(e,Nil()) case Cons(x,xs) => if (x <= e) Cons(x,buggySortedIns(e, xs)) else Cons(e, l) } - } ensuring(res => contents(res) == contents(l) ++ Set(e) + }.ensuring(res => contents(res) == contents(l) ++ Set(e) && isSorted(res) && size(res) == size(l) + 1 ) diff --git a/_static/invalid/ListOperations.scala b/_static/invalid/ListOperations.scala index 7ba835b52d..76a1601293 100644 --- a/_static/invalid/ListOperations.scala +++ b/_static/invalid/ListOperations.scala @@ -18,12 +18,12 @@ object ListOperations { def size(l: List) : BigInt = (l match { case Nil() => BigInt(0) case Cons(_, t) => 1 + size(t) - }) ensuring(res => res >= 0) + }).ensuring(res => res >= 0) def iplSize(l: IntPairList) : BigInt = (l match { case IPNil() => BigInt(0) case IPCons(_, xs) => 1 + iplSize(xs) - }) ensuring(_ >= 0) + }).ensuring(_ >= 0) def zip(l1: List, l2: List) : IntPairList = { // try to uncomment this and see how pattern-matching becomes exhaustive @@ -35,7 +35,7 @@ object ListOperations { case Cons(y, ys) => IPCons(IP(x, y), zip(xs, ys)) } } - } ensuring(iplSize(_) == size(l1)) + }.ensuring(iplSize(_) == size(l1)) def sizeTailRec(l: List) : BigInt = sizeTailRecAcc(l, 0) def sizeTailRecAcc(l: List, acc: BigInt) : BigInt = { @@ -44,7 +44,7 @@ object ListOperations { case Nil() => acc case Cons(_, xs) => sizeTailRecAcc(xs, acc+1) } - } ensuring(res => res == size(l) + acc) + }.ensuring(res => res == size(l) + acc) def sizesAreEquiv(l: List) : Boolean = { size(l) == sizeTailRec(l) @@ -62,18 +62,18 @@ object ListOperations { def drunk(l : List) : List = (l match { case Nil() => Nil() case Cons(x,l1) => Cons(x,Cons(x,drunk(l1))) - }) ensuring (size(_) == 2 * size(l)) + }).ensuring (size(_) == 2 * size(l)) - def reverse(l: List) : List = reverse0(l, Nil()) ensuring(content(_) == content(l)) + def reverse(l: List) : List = reverse0(l, Nil()).ensuring(content(_) == content(l)) def reverse0(l1: List, l2: List) : List = (l1 match { case Nil() => l2 case Cons(x, xs) => reverse0(xs, Cons(x, l2)) - }) ensuring(content(_) == content(l1) ++ content(l2)) + }).ensuring(content(_) == content(l1) ++ content(l2)) def append(l1 : List, l2 : List) : List = (l1 match { case Nil() => l2 case Cons(x,xs) => Cons(x, append(xs, l2)) - }) ensuring(content(_) == content(l1) ++ content(l2)) + }).ensuring(content(_) == content(l1) ++ content(l2)) @induct def nilAppend(l : List) : Boolean = (append(l, Nil()) == l).holds @@ -92,7 +92,7 @@ object ListOperations { @induct def concat(l1: List, l2: List) : List = - concat0(l1, l2, Nil()) ensuring(content(_) == content(l1) ++ content(l2)) + concat0(l1, l2, Nil()).ensuring(content(_) == content(l1) ++ content(l2)) @induct def concat0(l1: List, l2: List, l3: List) : List = (l1 match { @@ -103,5 +103,5 @@ object ListOperations { } } case Cons(x, xs) => concat0(xs, l2, Cons(x, l3)) - }) ensuring(content(_) == content(l1) ++ content(l2) ++ content(l3)) + }).ensuring(content(_) == content(l1) ++ content(l2) ++ content(l3)) } diff --git a/_static/invalid/Mean.scala b/_static/invalid/Mean.scala index c79ad49794..282386cbe4 100644 --- a/_static/invalid/Mean.scala +++ b/_static/invalid/Mean.scala @@ -8,6 +8,6 @@ object Mean { def meanOverflow(x: Int, y: Int): Int = { require(x <= y && x >= 0 && y >= 0) (x + y)/2 - } ensuring(m => m >= x && m <= y) + }.ensuring(m => m >= x && m <= y) } diff --git a/_static/invalid/PropositionalLogic.scala b/_static/invalid/PropositionalLogic.scala index 654a28d303..450778ee85 100644 --- a/_static/invalid/PropositionalLogic.scala +++ b/_static/invalid/PropositionalLogic.scala @@ -15,7 +15,7 @@ object PropositionalLogic { def simplify(f: Formula): Formula = (f match { case Implies(lhs, rhs) => Or(Not(simplify(lhs)), simplify(rhs)) case _ => f - }) ensuring(isSimplified(_)) + }).ensuring(isSimplified(_)) def isSimplified(f: Formula): Boolean = f match { case And(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs) diff --git a/_static/invalid/RedBlackTree2.scala b/_static/invalid/RedBlackTree2.scala index 6fc4b6cf74..0afb0fc766 100644 --- a/_static/invalid/RedBlackTree2.scala +++ b/_static/invalid/RedBlackTree2.scala @@ -24,7 +24,7 @@ object RedBlackTree2 { def size(t: Tree) : BigInt = (t match { case Empty() => BigInt(0) case Node(_, l, v, r) => size(l) + 1 + size(r) - }) ensuring(_ >= 0) + }).ensuring(_ >= 0) def isBlack(t: Tree) : Boolean = t match { case Empty() => true @@ -63,7 +63,7 @@ object RedBlackTree2 { else if (x == y) Node(c,a,y,b) else balance(c,a,y,ins(x, b)) } - } ensuring (res => content(res) == content(t) ++ Set(x) + }.ensuring(res => content(res) == content(t) ++ Set(x) && size(t) <= size(res) && size(res) <= size(t) + 1 && redDescHaveBlackChildren(res) && blackBalanced(res)) @@ -80,10 +80,10 @@ object RedBlackTree2 { Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d)) case Node(c,a,xV,b) => Node(c,a,xV,b) } - } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res)) + }.ensuring(res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res)) def buggyAdd(x: Int, t: Tree): Tree = { require(redNodesHaveBlackChildren(t)) ins(x, t) - } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res)) + }.ensuring(res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res)) } diff --git a/_static/invalid/SpecWithExtern.scala b/_static/invalid/SpecWithExtern.scala index 4480b715f1..f5884cf7f4 100644 --- a/_static/invalid/SpecWithExtern.scala +++ b/_static/invalid/SpecWithExtern.scala @@ -11,12 +11,12 @@ object SpecWithExtern { def randomBetween(l: Int, h: Int): Int = { require(l <= h) l - } ensuring(res => (res >= l && res <= h)) + }.ensuring(res => (res >= l && res <= h)) //postcondition is wrong, but if stainless considers //actual body of randomBetween it would be correct def wrongProp(): Int = { randomBetween(0, 10) - } ensuring(res => res >= 0 && res < 10) + }.ensuring(res => res >= 0 && res < 10) } diff --git a/_static/js/html5shiv-printshiv.min.js b/_static/js/html5shiv-printshiv.min.js new file mode 100644 index 0000000000..2b43bd062e --- /dev/null +++ b/_static/js/html5shiv-printshiv.min.js @@ -0,0 +1,4 @@ +/** +* @preserve HTML5 Shiv 3.7.3-pre | @afarkas @jdalton @jon_neal @rem | MIT/GPL2 Licensed +*/ +!function(a,b){function c(a,b){var c=a.createElement("p"),d=a.getElementsByTagName("head")[0]||a.documentElement;return c.innerHTML="x",d.insertBefore(c.lastChild,d.firstChild)}function d(){var a=y.elements;return"string"==typeof a?a.split(" "):a}function e(a,b){var c=y.elements;"string"!=typeof c&&(c=c.join(" ")),"string"!=typeof a&&(a=a.join(" ")),y.elements=c+" "+a,j(b)}function f(a){var b=x[a[v]];return b||(b={},w++,a[v]=w,x[w]=b),b}function g(a,c,d){if(c||(c=b),q)return c.createElement(a);d||(d=f(c));var e;return e=d.cache[a]?d.cache[a].cloneNode():u.test(a)?(d.cache[a]=d.createElem(a)).cloneNode():d.createElem(a),!e.canHaveChildren||t.test(a)||e.tagUrn?e:d.frag.appendChild(e)}function h(a,c){if(a||(a=b),q)return a.createDocumentFragment();c=c||f(a);for(var e=c.frag.cloneNode(),g=0,h=d(),i=h.length;i>g;g++)e.createElement(h[g]);return e}function i(a,b){b.cache||(b.cache={},b.createElem=a.createElement,b.createFrag=a.createDocumentFragment,b.frag=b.createFrag()),a.createElement=function(c){return y.shivMethods?g(c,a,b):b.createElem(c)},a.createDocumentFragment=Function("h,f","return function(){var n=f.cloneNode(),c=n.createElement;h.shivMethods&&("+d().join().replace(/[\w\-:]+/g,function(a){return b.createElem(a),b.frag.createElement(a),'c("'+a+'")'})+");return n}")(y,b.frag)}function j(a){a||(a=b);var d=f(a);return!y.shivCSS||p||d.hasCSS||(d.hasCSS=!!c(a,"article,aside,dialog,figcaption,figure,footer,header,hgroup,main,nav,section{display:block}mark{background:#FF0;color:#000}template{display:none}")),q||i(a,d),a}function k(a){for(var b,c=a.getElementsByTagName("*"),e=c.length,f=RegExp("^(?:"+d().join("|")+")$","i"),g=[];e--;)b=c[e],f.test(b.nodeName)&&g.push(b.applyElement(l(b)));return g}function l(a){for(var b,c=a.attributes,d=c.length,e=a.ownerDocument.createElement(A+":"+a.nodeName);d--;)b=c[d],b.specified&&e.setAttribute(b.nodeName,b.nodeValue);return e.style.cssText=a.style.cssText,e}function m(a){for(var b,c=a.split("{"),e=c.length,f=RegExp("(^|[\\s,>+~])("+d().join("|")+")(?=[[\\s,>+~#.:]|$)","gi"),g="$1"+A+"\\:$2";e--;)b=c[e]=c[e].split("}"),b[b.length-1]=b[b.length-1].replace(f,g),c[e]=b.join("}");return c.join("{")}function n(a){for(var b=a.length;b--;)a[b].removeNode()}function o(a){function b(){clearTimeout(g._removeSheetTimer),d&&d.removeNode(!0),d=null}var d,e,g=f(a),h=a.namespaces,i=a.parentWindow;return!B||a.printShived?a:("undefined"==typeof h[A]&&h.add(A),i.attachEvent("onbeforeprint",function(){b();for(var f,g,h,i=a.styleSheets,j=[],l=i.length,n=Array(l);l--;)n[l]=i[l];for(;h=n.pop();)if(!h.disabled&&z.test(h.media)){try{f=h.imports,g=f.length}catch(o){g=0}for(l=0;g>l;l++)n.push(f[l]);try{j.push(h.cssText)}catch(o){}}j=m(j.reverse().join("")),e=k(a),d=c(a,j)}),i.attachEvent("onafterprint",function(){n(e),clearTimeout(g._removeSheetTimer),g._removeSheetTimer=setTimeout(b,500)}),a.printShived=!0,a)}var p,q,r="3.7.3",s=a.html5||{},t=/^<|^(?:button|map|select|textarea|object|iframe|option|optgroup)$/i,u=/^(?:a|b|code|div|fieldset|h1|h2|h3|h4|h5|h6|i|label|li|ol|p|q|span|strong|style|table|tbody|td|th|tr|ul)$/i,v="_html5shiv",w=0,x={};!function(){try{var a=b.createElement("a");a.innerHTML="').appendTo(this.out); - this.output = $('
' + + '' + + _("Hide Search Matches") + + "
" + ) + ); + }, + + /** + * helper function to hide the search marks again + */ + hideSearchWords: () => { + document + .querySelectorAll("#searchbox .highlight-link") + .forEach((el) => el.remove()); + document + .querySelectorAll("span.highlighted") + .forEach((el) => el.classList.remove("highlighted")); + localStorage.removeItem("sphinx_highlight_terms") + }, + + initEscapeListener: () => { + // only install a listener if it is really needed + if (!DOCUMENTATION_OPTIONS.ENABLE_SEARCH_SHORTCUTS) return; + + document.addEventListener("keydown", (event) => { + // bail for input elements + if (BLACKLISTED_KEY_CONTROL_ELEMENTS.has(document.activeElement.tagName)) return; + // bail with special keys + if (event.shiftKey || event.altKey || event.ctrlKey || event.metaKey) return; + if (DOCUMENTATION_OPTIONS.ENABLE_SEARCH_SHORTCUTS && (event.key === "Escape")) { + SphinxHighlight.hideSearchWords(); + event.preventDefault(); + } + }); + }, +}; + +_ready(() => { + /* Do not call highlightSearchWords() when we are on the search page. + * It will highlight words from the *previous* search query. + */ + if (typeof Search === "undefined") SphinxHighlight.highlightSearchWords(); + SphinxHighlight.initEscapeListener(); +}); diff --git a/_static/valid/AbstractRefinementMap.scala b/_static/valid/AbstractRefinementMap.scala index 48cb2ec848..3299b699e9 100644 --- a/_static/valid/AbstractRefinementMap.scala +++ b/_static/valid/AbstractRefinementMap.scala @@ -12,7 +12,7 @@ object AbstractRefinementMap { def apply(x: A): B = { require(f.pre(x)) f(x) - } ensuring(ens) + }.ensuring(ens) } def map[A, B](l: List[A], f: A ~> B): List[B] = { @@ -21,6 +21,6 @@ object AbstractRefinementMap { case Cons(x, xs) => Cons[B](f(x), map(xs, f)) case Nil() => Nil[B]() } - } ensuring { res => forall((x: B) => res.contains(x) ==> f.ens(x)) } + }.ensuring { res => forall((x: B) => res.contains(x) ==> f.ens(x)) } } diff --git a/_static/valid/AddingPositiveNumbers.scala b/_static/valid/AddingPositiveNumbers.scala index 84fca5dc63..5452a5811b 100644 --- a/_static/valid/AddingPositiveNumbers.scala +++ b/_static/valid/AddingPositiveNumbers.scala @@ -6,6 +6,6 @@ object AddingPositiveNumbers { def additionSound(x: BigInt, y: BigInt): BigInt = { require(x >= 0 && y >= 0) x + y - } ensuring(_ >= 0) + }.ensuring(_ >= 0) } diff --git a/_static/valid/AssociativeList.scala b/_static/valid/AssociativeList.scala index 45ac711a12..0ac55c0d90 100644 --- a/_static/valid/AssociativeList.scala +++ b/_static/valid/AssociativeList.scala @@ -33,14 +33,14 @@ object AssociativeList { def updateAll(l1: List, l2: List): List = (l2 match { case Nil() => l1 case Cons(x, xs) => updateAll(updateElem(l1, x), xs) - }) ensuring(domain(_) == domain(l1) ++ domain(l2)) + }).ensuring(domain(_) == domain(l1) ++ domain(l2)) def updateElem(l: List, e: KeyValuePairAbs): List = (l match { case Nil() => Cons(e, Nil()) case Cons(KeyValuePair(k, v), xs) => e match { case KeyValuePair(ek, ev) => if (ek == k) Cons(KeyValuePair(ek, ev), xs) else Cons(KeyValuePair(k, v), updateElem(xs, e)) } - }) ensuring(res => e match { + }).ensuring(res => e match { case KeyValuePair(k, v) => domain(res) == domain(l) ++ Set[Int](k) }) diff --git a/_static/valid/BinarySearchTreeQuant.scala b/_static/valid/BinarySearchTreeQuant.scala index 36f80d7d8b..638b3652cd 100644 --- a/_static/valid/BinarySearchTreeQuant.scala +++ b/_static/valid/BinarySearchTreeQuant.scala @@ -36,9 +36,9 @@ object BSTSimpler { Node(l, v, r) }) } - } ensuring(res => isBST(res) && content(res) == content(tree) ++ Set(value)) + }.ensuring(res => isBST(res) && content(res) == content(tree) ++ Set(value)) def createRoot(v: BigInt): Node = { Node(Leaf(), v, Leaf()) - } ensuring (content(_) == Set(v)) + }.ensuring(content(_) == Set(v)) } diff --git a/_static/valid/ChooseWithWitness.scala b/_static/valid/ChooseWithWitness.scala index 3d6c1c1d31..57df8db6bd 100644 --- a/_static/valid/ChooseWithWitness.scala +++ b/_static/valid/ChooseWithWitness.scala @@ -11,7 +11,7 @@ object ChooseWithWitness { def size(l: List) : BigInt = (l match { case Nil() => BigInt(0) case Cons(_, t) => 1 + size(t) - }) ensuring(res => res >= 0) + }).ensuring(res => res >= 0) def content(l: List) : Set[Int] = l match { case Nil() => Set.empty[Int] @@ -26,7 +26,7 @@ object ChooseWithWitness { } else { Cons(0, createListOfSize(i - 1)) } - } ensuring ( size(_) == i ) + }.ensuring( size(_) == i ) def listOfSize(i: BigInt): List = { require(i >= 0) @@ -37,7 +37,7 @@ object ChooseWithWitness { assert(size(createListOfSize(i)) == i) // provides choose quantification with a matcher choose[List] { (res: List) => size(res) == i } } - } ensuring ( size(_) == i ) + }.ensuring( size(_) == i ) def listOfSize2(i: BigInt): List = { require(i >= 0) @@ -47,5 +47,5 @@ object ChooseWithWitness { } else { Nil() } - } ensuring ( size(_) == i ) + }.ensuring( size(_) == i ) } diff --git a/_static/valid/ConcRope.scala b/_static/valid/ConcRope.scala index 932bd11494..79606df433 100644 --- a/_static/valid/ConcRope.scala +++ b/_static/valid/ConcRope.scala @@ -84,7 +84,7 @@ object ConcRope { case Append(l, r) => 1 + max(l.level, r.level) }): BigInt - } ensuring (_ >= 0) + }.ensuring(_ >= 0) val size: BigInt = { (this match { @@ -95,7 +95,7 @@ object ConcRope { case Append(l, r) => l.size + r.size }): BigInt - } ensuring (_ >= 0) + }.ensuring(_ >= 0) def toList: List[T] = { this match { @@ -106,7 +106,7 @@ object ConcRope { case Append(l, r) => l.toList ++ r.toList } - } ensuring (res => res.size == this.size) + }.ensuring(res => res.size == this.size) } case class Empty[T]() extends Conc[T] @@ -125,7 +125,7 @@ object ConcRope { if (i < l.size) lookup(l, i) else lookup(r, i - l.size) } - } ensuring (res => instAppendIndexAxiom(xs, i) && // an auxiliary axiom instantiation that required for the proof + }.ensuring(res => instAppendIndexAxiom(xs, i) && // an auxiliary axiom instantiation that required for the proof res == xs.toList(i)) // correctness @@ -153,7 +153,7 @@ object ConcRope { } else Append(l, update(r, i - l.size, y)) } - } ensuring (res => instAppendUpdateAxiom(xs, i, y) && // an auxiliary axiom instantiation + }.ensuring(res => instAppendUpdateAxiom(xs, i, y) && // an auxiliary axiom instantiation res.level == xs.level && // heights of the input and output trees are equal res.valid && // tree invariants are preserved res.toList == xs.toList.updated(i, y) && // correctness @@ -191,7 +191,7 @@ object ConcRope { case _ => concatNonEmpty(xs, ys) } - } ensuring (res => res.valid && // tree invariants + }.ensuring(res => res.valid && // tree invariants res.level <= max(xs.level, ys.level) + 1 && // height invariants res.level >= max(xs.level, ys.level) && (res.toList == xs.toList ++ ys.toList) && // correctness @@ -242,7 +242,7 @@ object ConcRope { } } } - } ensuring (res => + }.ensuring(res => appendAssocInst(xs, ys) && // instantiation of an axiom res.level <= max(xs.level, ys.level) + 1 && // height invariants res.level >= max(xs.level, ys.level) && @@ -294,7 +294,7 @@ object ConcRope { case CC(l, r) => concatNonEmpty(l, insert(r, i - l.size, y)) } - } ensuring (res => insertAppendAxiomInst(xs, i, y) && // instantiation of an axiom + }.ensuring(res => insertAppendAxiomInst(xs, i, y) && // instantiation of an axiom res.valid && res.isNormalized && // tree invariants res.level - xs.level <= 1 && res.level >= xs.level && // height of the output tree is at most 1 greater than that of the input tree res.toList == insertAtIndex(xs.toList, i, y) // correctness @@ -359,7 +359,7 @@ object ConcRope { (l, r) } } - } ensuring (res => instSplitAxiom(xs, n) && // instantiation of an axiom + }.ensuring(res => instSplitAxiom(xs, n) && // instantiation of an axiom res._1.valid && res._2.valid && // tree invariants are preserved res._1.isNormalized && res._2.isNormalized && xs.level >= res._1.level && xs.level >= res._2.level && // height bounds of the resulting tree @@ -385,7 +385,7 @@ object ConcRope { case Empty() => ys case Single(_) => CC(xs, ys) } - } ensuring (res => res.valid && //conctree invariants + }.ensuring(res => res.valid && //conctree invariants res.toList == xs.toList ++ Cons(x, Nil[T]()) && //correctness res.level <= xs.level + 1 ) @@ -411,7 +411,7 @@ object ConcRope { Append(l, zs) } } - } ensuring (res => appendAssocInst2(xs, ys) && + }.ensuring(res => appendAssocInst2(xs, ys) && res.valid && //conc tree invariants res.toList == xs.toList ++ ys.toList && //correctness invariants res.level <= xs.level + 1 ) @@ -431,7 +431,7 @@ object ConcRope { case Append(l, r) => numTrees(l) + 1 case _ => BigInt(1) } - } ensuring (res => res >= 0) + }.ensuring(res => res >= 0) def normalize[T](t: Conc[T]): Conc[T] = { require(t.valid) @@ -442,7 +442,7 @@ object ConcRope { concatNormalized(l, r) case _ => t } - } ensuring (res => res.valid && + }.ensuring(res => res.valid && res.isNormalized && res.toList == t.toList && //correctness res.size == t.size && res.level <= t.level //normalize preserves level and size @@ -457,7 +457,7 @@ object ConcRope { case l => concatNormalized(l, nr) } - } ensuring (res => + }.ensuring(res => appendAssocInst2(xs, ys) && //some lemma instantiations res.valid && res.isNormalized && diff --git a/_static/valid/Formulas.scala b/_static/valid/Formulas.scala index a5a350d827..4c011e4373 100644 --- a/_static/valid/Formulas.scala +++ b/_static/valid/Formulas.scala @@ -45,7 +45,7 @@ object Formulas { case Not(e) => Not(desugar(e)) case e => e } - } ensuring { out => + }.ensuring { out => !existsImplies(out) && !exists(out, f => f.isInstanceOf[Implies]) } diff --git a/_static/valid/FunctionCaching.scala b/_static/valid/FunctionCaching.scala index 5e0984b3aa..3d089e4599 100644 --- a/_static/valid/FunctionCaching.scala +++ b/_static/valid/FunctionCaching.scala @@ -14,7 +14,7 @@ object FunctionCaching { case Some(cached) => cached } - } ensuring(res => old(funCache).cached.get(x) match { + }.ensuring(res => old(funCache).cached.get(x) match { case None() => true case Some(v) => v == res }) @@ -35,6 +35,6 @@ object FunctionCaching { fun(y) multipleCalls(ys, x) } - } ensuring(_ => funCache.cached.get(x).forall(_ == 2*x + 42)) + }.ensuring(_ => funCache.cached.get(x).forall(_ == 2*x + 42)) } diff --git a/_static/valid/Heaps.scala b/_static/valid/Heaps.scala index b16418adb3..5f65056b88 100644 --- a/_static/valid/Heaps.scala +++ b/_static/valid/Heaps.scala @@ -36,7 +36,7 @@ object Heaps { private def reverse0(h : Heap, acc : Heap) : Heap = (h match { case Empty => acc case Nodes(n, ns) => reverse0(ns, Nodes(n, acc)) - }) ensuring(res => heapContent(res) == heapContent(h) ++ heapContent(acc)) + }).ensuring(res => heapContent(res) == heapContent(h) ++ heapContent(acc)) private def link(t1 : Node, t2 : Node) = (t1, t2) match { case (Node(r, e1, ns1), Node(_, e2, ns2)) => @@ -55,7 +55,7 @@ object Heaps { } else { insertNode(link(t, t2), h2) } - }) ensuring(res => heapContent(res) == nodeContent(t) ++ heapContent(h)) + }).ensuring(res => heapContent(res) == nodeContent(t) ++ heapContent(h)) private def getMin(h : Heap) : (Node, Heap) = { require(h != Empty) @@ -69,7 +69,7 @@ object Heaps { (t0, Nodes(t, ts0)) } } - } ensuring(_ match { + }.ensuring(_ match { case (n,h2) => nodeContent(n) ++ heapContent(h2) == heapContent(h) }) @@ -78,15 +78,15 @@ object Heaps { /*~~~~~~~~~~~~~~~~*/ def empty() : Heap = { Empty - } ensuring(res => heapContent(res) == Set.empty[Int]) + }.ensuring(res => heapContent(res) == Set.empty[Int]) def isEmpty(h : Heap) : Boolean = { (h == Empty) - } ensuring(res => res == (heapContent(h) == Set.empty[Int])) + }.ensuring(res => res == (heapContent(h) == Set.empty[Int])) def insert(e : Int, h : Heap) : Heap = { insertNode(Node(0, e, Empty), h) - } ensuring(res => heapContent(res) == heapContent(h) ++ Set(e)) + }.ensuring(res => heapContent(res) == heapContent(h) ++ Set(e)) def merge(h1 : Heap, h2 : Heap) : Heap = ((h1,h2) match { case (_, Empty) => h1 @@ -99,7 +99,7 @@ object Heaps { } else { insertNode(link(t1, t2), merge(ts1, ts2)) } - }) ensuring(res => heapContent(res) == heapContent(h1) ++ heapContent(h2)) + }).ensuring(res => heapContent(res) == heapContent(h1) ++ heapContent(h2)) def findMin(h : Heap) : OptInt = (h match { case Empty => None @@ -108,7 +108,7 @@ object Heaps { case None => Some(e) case Some(e2) => Some(if(e < e2) e else e2) } - }) ensuring(_ match { + }).ensuring(_ match { case None => isEmpty(h) case Some(v) => heapContent(h).contains(v) }) @@ -118,7 +118,7 @@ object Heaps { case ts : Nodes => val (Node(_, e, ns1), ns2) = getMin(ts) merge(reverse(ns1), ns2) - }) ensuring(res => heapContent(res).subsetOf(heapContent(h))) + }).ensuring(res => heapContent(res).subsetOf(heapContent(h))) def sanity0() : Boolean = { val h0 : Heap = Empty diff --git a/_static/valid/InsertionSort.scala b/_static/valid/InsertionSort.scala index 0acab72588..bed8b1d5fa 100644 --- a/_static/valid/InsertionSort.scala +++ b/_static/valid/InsertionSort.scala @@ -15,7 +15,7 @@ object InsertionSort { def size(l : List) : BigInt = (l match { case Nil() => BigInt(0) case Cons(_, xs) => 1 + size(xs) - }) ensuring(_ >= 0) + }).ensuring(_ >= 0) def contents(l: List): Set[Int] = l match { case Nil() => Set.empty @@ -44,7 +44,7 @@ object InsertionSort { case Nil() => Cons(e,Nil()) case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l) } - } ensuring(res => contents(res) == contents(l) ++ Set(e) + }.ensuring(res => contents(res) == contents(l) ++ Set(e) && isSorted(res) && size(res) == size(l) + 1 ) @@ -54,7 +54,7 @@ object InsertionSort { def sort(l: List): List = (l match { case Nil() => Nil() case Cons(x,xs) => sortedIns(x, sort(xs)) - }) ensuring(res => contents(res) == contents(l) + }).ensuring(res => contents(res) == contents(l) && isSorted(res) && size(res) == size(l) ) diff --git a/_static/valid/ListOperations.scala b/_static/valid/ListOperations.scala index 3a4383cc9b..aafe68ea7e 100644 --- a/_static/valid/ListOperations.scala +++ b/_static/valid/ListOperations.scala @@ -18,12 +18,12 @@ object ListOperations { def size(l: List) : BigInt = (l match { case Nil() => BigInt(0) case Cons(_, t) => 1 + size(t) - }) ensuring(res => res >= 0) + }).ensuring(res => res >= 0) def iplSize(l: IntPairList) : BigInt = (l match { case IPNil() => BigInt(0) case IPCons(_, xs) => 1 + iplSize(xs) - }) ensuring(_ >= 0) + }).ensuring(_ >= 0) def zip(l1: List, l2: List) : IntPairList = { // try to comment this and see how pattern-matching becomes @@ -36,7 +36,7 @@ object ListOperations { case Cons(y, ys) => IPCons(IP(x, y), zip(xs, ys)) } } - } ensuring(iplSize(_) == size(l1)) + }.ensuring(iplSize(_) == size(l1)) def sizeTailRec(l: List) : BigInt = sizeTailRecAcc(l, 0) def sizeTailRecAcc(l: List, acc: BigInt) : BigInt = { @@ -45,7 +45,7 @@ object ListOperations { case Nil() => acc case Cons(_, xs) => sizeTailRecAcc(xs, acc+1) } - } ensuring(res => res == size(l) + acc) + }.ensuring(res => res == size(l) + acc) def sizesAreEquiv(l: List) : Boolean = { size(l) == sizeTailRec(l) @@ -63,18 +63,18 @@ object ListOperations { def drunk(l : List) : List = (l match { case Nil() => Nil() case Cons(x,l1) => Cons(x,Cons(x,drunk(l1))) - }) ensuring (size(_) == 2 * size(l)) + }).ensuring (size(_) == 2 * size(l)) - def reverse(l: List) : List = reverse0(l, Nil()) ensuring(content(_) == content(l)) + def reverse(l: List) : List = reverse0(l, Nil()).ensuring(content(_) == content(l)) def reverse0(l1: List, l2: List) : List = (l1 match { case Nil() => l2 case Cons(x, xs) => reverse0(xs, Cons(x, l2)) - }) ensuring(content(_) == content(l1) ++ content(l2)) + }).ensuring(content(_) == content(l1) ++ content(l2)) def append(l1 : List, l2 : List) : List = (l1 match { case Nil() => l2 case Cons(x,xs) => Cons(x, append(xs, l2)) - }) ensuring(content(_) == content(l1) ++ content(l2)) + }).ensuring(content(_) == content(l1) ++ content(l2)) @induct def nilAppend(l : List) : Boolean = (append(l, Nil()) == l).holds @@ -89,7 +89,7 @@ object ListOperations { @induct def concat(l1: List, l2: List) : List = - concat0(l1, l2, Nil()) ensuring(content(_) == content(l1) ++ content(l2)) + concat0(l1, l2, Nil()).ensuring(content(_) == content(l1) ++ content(l2)) @induct def concat0(l1: List, l2: List, l3: List) : List = (l1 match { @@ -100,5 +100,5 @@ object ListOperations { } } case Cons(x, xs) => concat0(xs, l2, Cons(x, l3)) - }) ensuring(content(_) == content(l1) ++ content(l2) ++ content(l3)) + }).ensuring(content(_) == content(l1) ++ content(l2) ++ content(l3)) } diff --git a/_static/valid/Mean.scala b/_static/valid/Mean.scala index ec1108f4e5..85b229498c 100644 --- a/_static/valid/Mean.scala +++ b/_static/valid/Mean.scala @@ -8,6 +8,6 @@ object Mean { def mean(x: Int, y: Int): Int = { require(x <= y && x >= 0 && y >= 0) x + (y - x)/2 - } ensuring(m => m >= x && m <= y) + }.ensuring(m => m >= x && m <= y) } diff --git a/_static/valid/MergeSort.scala b/_static/valid/MergeSort.scala index b4cd205689..dbcdf93a91 100644 --- a/_static/valid/MergeSort.scala +++ b/_static/valid/MergeSort.scala @@ -26,7 +26,7 @@ object MergeSort { def size(list : List) : BigInt = (list match { case Nil() => BigInt(0) case Cons(_, xs) => 1 + size(xs) - }) ensuring(_ >= 0) + }).ensuring(_ >= 0) def isSorted(list : List) : Boolean = list match { case Nil() => true @@ -42,7 +42,7 @@ object MergeSort { def abs(i : BigInt) : BigInt = { if(i < 0) -i else i - } ensuring(_ >= 0) + }.ensuring(_ >= 0) def mergeSpec(list1 : List, list2 : List, res : List) : Boolean = { isSorted(res) && content(res) == content(list1) ++ content(list2) @@ -61,7 +61,7 @@ object MergeSort { Cons(y, mergeFast(list1, ys)) } } - } ensuring(res => mergeSpec(list1, list2, res)) + }.ensuring(res => mergeSpec(list1, list2, res)) def splitSpec(list : List, res : (List,List)) : Boolean = { val s1 = size(res._1) @@ -76,7 +76,7 @@ object MergeSort { case Cons(x1, Cons(x2, xs)) => val (s1,s2) = split(xs) (Cons(x1, s1), Cons(x2, s2)) - }) ensuring(res => splitSpec(list, res)) + }).ensuring(res => splitSpec(list, res)) def sortSpec(in : List, out : List) : Boolean = { content(out) == content(in) && isSorted(out) @@ -94,12 +94,12 @@ object MergeSort { val (s1,s2) = split(in) mergeFast(weirdSort(size(s1), s1), weirdSort(size(s2), s2)) } - } ensuring(res => sortSpec(in, res)) + }.ensuring(res => sortSpec(in, res)) def toLList(list : List) : LList = (list match { case Nil() => LNil() case Cons(x, xs) => LCons(Cons(x, Nil()), toLList(xs)) - }) ensuring(res => lContent(res) == content(list) && lIsSorted(res)) + }).ensuring(res => lContent(res) == content(list) && lIsSorted(res)) def mergeMap(llist : LList) : LList = { require(lIsSorted(llist)) @@ -109,7 +109,7 @@ object MergeSort { case o @ LCons(x, LNil()) => o case LCons(x, LCons(y, ys)) => LCons(mergeFast(x, y), mergeMap(ys)) } - } ensuring(res => lContent(res) == lContent(llist) && lIsSorted(res)) + }.ensuring(res => lContent(res) == lContent(llist) && lIsSorted(res)) def mergeReduce(llist : LList) : List = { require(lIsSorted(llist)) @@ -119,9 +119,9 @@ object MergeSort { case LCons(x, LNil()) => x case _ => mergeReduce(mergeMap(llist)) } - } ensuring(res => content(res) == lContent(llist) && isSorted(res)) + }.ensuring(res => content(res) == lContent(llist) && isSorted(res)) def mergeSort(in : List) : List = { mergeReduce(toLList(in)) - } ensuring(res => sortSpec(in, res)) + }.ensuring(res => sortSpec(in, res)) } diff --git a/_static/valid/PropositionalLogic.scala b/_static/valid/PropositionalLogic.scala index d1a4a4a460..aab240a9b0 100644 --- a/_static/valid/PropositionalLogic.scala +++ b/_static/valid/PropositionalLogic.scala @@ -18,7 +18,7 @@ object PropositionalLogic { case Implies(lhs, rhs) => Or(Not(simplify(lhs)), simplify(rhs)) case Not(f) => Not(simplify(f)) case Literal(_) => f - }) ensuring(isSimplified(_)) + }).ensuring(isSimplified(_)) def isSimplified(f: Formula): Boolean = f match { case And(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs) @@ -38,7 +38,7 @@ object PropositionalLogic { case Not(Not(f)) => nnf(f) case Not(Literal(_)) => formula case Literal(_) => formula - }) ensuring(isNNF(_)) + }).ensuring(isNNF(_)) def isNNF(f: Formula): Boolean = f match { case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs) diff --git a/_static/valid/QuickSort.scala b/_static/valid/QuickSort.scala index 9cd49876e8..46bfd9f4a6 100644 --- a/_static/valid/QuickSort.scala +++ b/_static/valid/QuickSort.scala @@ -17,7 +17,7 @@ object QuickSort { case Nil() => l2 case Cons(x, xs) => Cons(x, appendSorted(xs, l2)) } - } ensuring { res => + }.ensuring { res => isSorted(res) && res.content == l1.content ++ l2.content } @@ -28,7 +28,7 @@ object QuickSort { case Nil() => Nil[BigInt]() case Cons(x, xs) => par(x, Nil(), Nil(), xs) } - } ensuring { res => + }.ensuring { res => isSorted(res) && res.content == list.content } @@ -44,7 +44,7 @@ object QuickSort { case Nil() => appendSorted(quickSort(l), Cons(x, quickSort(r))) case Cons(x2, xs2) => if (x2 <= x) par(x, Cons(x2, l), r, xs2) else par(x, l, Cons(x2, r), xs2) } - } ensuring { res => + }.ensuring { res => isSorted(res) && res.content == l.content ++ r.content ++ ls.content + x } diff --git a/_static/valid/RedBlackTree.scala b/_static/valid/RedBlackTree.scala index 94577704d6..4b7fab2dc6 100644 --- a/_static/valid/RedBlackTree.scala +++ b/_static/valid/RedBlackTree.scala @@ -24,7 +24,7 @@ object RedBlackTree { def size(t: Tree) : BigInt = (t match { case Empty() => BigInt(0) case Node(_, l, v, r) => size(l) + 1 + size(r) - }) ensuring(_ >= 0) + }).ensuring(_ >= 0) /* We consider leaves to be black by definition */ def isBlack(t: Tree) : Boolean = t match { @@ -65,7 +65,7 @@ object RedBlackTree { else if (x == y) Node(c,a,y,b) else balance(c,a,y,ins(x, b)) } - } ensuring (res => content(res) == content(t) ++ Set(x) + }.ensuring(res => content(res) == content(t) ++ Set(x) && size(t) <= size(res) && size(res) <= size(t) + 1 && redDescHaveBlackChildren(res) && blackBalanced(res)) @@ -76,12 +76,12 @@ object RedBlackTree { case Node(Red(),l,v,r) => Node(Black(),l,v,r) case _ => n } - } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res)) + }.ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res)) def add(x: BigInt, t: Tree): Tree = { require(redNodesHaveBlackChildren(t) && blackBalanced(t)) makeBlack(ins(x, t)) - } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res)) + }.ensuring(res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res)) def balance(c: Color, a: Tree, x: BigInt, b: Tree): Tree = { Node(c,a,x,b) match { @@ -95,5 +95,5 @@ object RedBlackTree { Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d)) case Node(c,a,xV,b) => Node(c,a,xV,b) } - } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res)) + }.ensuring(res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res)) } diff --git a/_static/valid/StableSorter.scala b/_static/valid/StableSorter.scala index 699b853cf3..1f07d89860 100644 --- a/_static/valid/StableSorter.scala +++ b/_static/valid/StableSorter.scala @@ -12,7 +12,7 @@ object StableSorter { case Cons(hd, tl) if key(t) <= key(hd) => t :: l case Cons(hd, tl) => hd :: insert(t, tl, key) } - } ensuring { res => res.content == Set(t) ++ l.content && res.length == 1 + l.length } + }.ensuring { res => res.content == Set(t) ++ l.content && res.length == 1 + l.length } // Sorting a list preserves the content and preserves the length def sort[T](l: List[T], key: T => BigInt): List[T] = { l match { @@ -21,7 +21,7 @@ object StableSorter { val tlSorted = sort(tl, key) insert(hd, tlSorted, key) } - }} ensuring { res => res.content == l.content && res.length == l.length } + }}.ensuring { res => res.content == l.content && res.length == l.length } // To define stability, we first annotate the input list with the initial indices... def annotateList[T](l: List[T], n: BigInt): List[(T, BigInt)] = { @@ -32,7 +32,7 @@ object StableSorter { hint((hd, n) :: tlAnn, trivProp2(annotateList(tl, n + 1), n)) } } - } ensuring { res => l2AtLeast(res, n) } + }.ensuring { res => l2AtLeast(res, n) } // ... where: def l2AtLeast[T](l: List[(T, BigInt)], n: BigInt): Boolean = l match { diff --git a/casestudies.html b/casestudies.html index 0eccdae54c..469dc11e6c 100644 --- a/casestudies.html +++ b/casestudies.html @@ -1,24 +1,23 @@ - + - +