Document not found (404)
+This URL is invalid, sorry. Please use the navigation bar or search to continue.
+ +"),i.setHtml(f),i.show(),t._signal("showGutterTooltip",i),t.on("mousewheel",c);if(e.$tooltipFollowsMouse)h(u);else{var p=u.domEvent.target,d=p.getBoundingClientRect(),v=i.getElement().style;v.left=d.right+"px",v.top=d.bottom+"px"}}function c(){o&&(o=clearTimeout(o)),f&&(i.hide(),f=null,t._signal("hideGutterTooltip",i),t.removeEventListener("mousewheel",c))}function h(e){i.setPosition(e.x,e.y)}var t=e.editor,n=t.renderer.$gutterLayer,i=new a(t.container);e.editor.setDefaultHandler("guttermousedown",function(r){if(!t.isFocused()||r.getButton()!=0)return;var i=n.getRegion(r);if(i=="foldWidgets")return;var s=r.getDocumentPosition().row,o=t.session.selection;if(r.getShiftKey())o.selectTo(s,0);else{if(r.domEvent.detail==2)return t.selectAll(),r.preventDefault();e.$clickSelection=t.selection.getLineRange(s)}return e.setState("selectByLines"),e.captureMouse(r),r.preventDefault()});var o,u,f;e.editor.setDefaultHandler("guttermousemove",function(t){var n=t.domEvent.target||t.domEvent.srcElement;if(r.hasCssClass(n,"ace_fold-widget"))return c();f&&e.$tooltipFollowsMouse&&h(t),u=t;if(o)return;o=setTimeout(function(){o=null,u&&!e.isMousePressed?l():c()},50)}),s.addListener(t.renderer.$gutter,"mouseout",function(e){u=null;if(!f||o)return;o=setTimeout(function(){o=null,c()},50)}),t.on("changeSession",c)}function a(e){o.call(this,e)}var r=e("../lib/dom"),i=e("../lib/oop"),s=e("../lib/event"),o=e("../tooltip").Tooltip;i.inherits(a,o),function(){this.setPosition=function(e,t){var n=window.innerWidth||document.documentElement.clientWidth,r=window.innerHeight||document.documentElement.clientHeight,i=this.getWidth(),s=this.getHeight();e+=15,t+=15,e+i>n&&(e-=e+i-n),t+s>r&&(t-=20+s),o.prototype.setPosition.call(this,e,t)}}.call(a.prototype),t.GutterHandler=u}),ace.define("ace/mouse/mouse_event",["require","exports","module","ace/lib/event","ace/lib/useragent"],function(e,t,n){"use strict";var r=e("../lib/event"),i=e("../lib/useragent"),s=t.MouseEvent=function(e,t){this.domEvent=e,this.editor=t,this.x=this.clientX=e.clientX,this.y=this.clientY=e.clientY,this.$pos=null,this.$inSelection=null,this.propagationStopped=!1,this.defaultPrevented=!1};(function(){this.stopPropagation=function(){r.stopPropagation(this.domEvent),this.propagationStopped=!0},this.preventDefault=function(){r.preventDefault(this.domEvent),this.defaultPrevented=!0},this.stop=function(){this.stopPropagation(),this.preventDefault()},this.getDocumentPosition=function(){return this.$pos?this.$pos:(this.$pos=this.editor.renderer.screenToTextCoordinates(this.clientX,this.clientY),this.$pos)},this.inSelection=function(){if(this.$inSelection!==null)return this.$inSelection;var e=this.editor,t=e.getSelectionRange();if(t.isEmpty())this.$inSelection=!1;else{var n=this.getDocumentPosition();this.$inSelection=t.contains(n.row,n.column)}return this.$inSelection},this.getButton=function(){return r.getButton(this.domEvent)},this.getShiftKey=function(){return this.domEvent.shiftKey},this.getAccelKey=i.isMac?function(){return this.domEvent.metaKey}:function(){return this.domEvent.ctrlKey}}).call(s.prototype)}),ace.define("ace/mouse/dragdrop_handler",["require","exports","module","ace/lib/dom","ace/lib/event","ace/lib/useragent"],function(e,t,n){"use strict";function f(e){function T(e,n){var r=Date.now(),i=!n||e.row!=n.row,s=!n||e.column!=n.column;if(!S||i||s)t.moveCursorToPosition(e),S=r,x={x:p,y:d};else{var o=l(x.x,x.y,p,d);o>a?S=null:r-S>=u&&(t.renderer.scrollCursorIntoView(),S=null)}}function N(e,n){var r=Date.now(),i=t.renderer.layerConfig.lineHeight,s=t.renderer.layerConfig.characterWidth,u=t.renderer.scroller.getBoundingClientRect(),a={x:{left:p-u.left,right:u.right-p},y:{top:d-u.top,bottom:u.bottom-d}},f=Math.min(a.x.left,a.x.right),l=Math.min(a.y.top,a.y.bottom),c={row:e.row,column:e.column};f/s<=2&&(c.column+=a.x.left
"),p.appendChild(i.createElement("div"));var m=function(e,t,n){if(t===0&&(n==="esc"||n==="return"))return h.destroy(),{command:"null"}};h.destroy=function(){if(e.$mouseHandler.isMousePressed)return;e.keyBinding.removeKeyboardHandler(m),n.widgetManager.removeLineWidget(h),e.off("changeSelection",h.destroy),e.off("changeSession",h.destroy),e.off("mouseup",h.destroy),e.off("change",h.destroy)},e.keyBinding.addKeyboardHandler(m),e.on("changeSelection",h.destroy),e.on("changeSession",h.destroy),e.on("mouseup",h.destroy),e.on("change",h.destroy),e.session.widgetManager.addLineWidget(h),h.el.onmousedown=e.focus.bind(e),e.renderer.scrollCursorIntoView(null,.5,{bottom:h.el.offsetHeight})},i.importCssString(" .error_widget_wrapper { background: inherit; color: inherit; border:none } .error_widget { border-top: solid 2px; border-bottom: solid 2px; margin: 5px 0; padding: 10px 40px; white-space: pre-wrap; } .error_widget.ace_error, .error_widget_arrow.ace_error{ border-color: #ff5a5a } .error_widget.ace_warning, .error_widget_arrow.ace_warning{ border-color: #F1D817 } .error_widget.ace_info, .error_widget_arrow.ace_info{ border-color: #5a5a5a } .error_widget.ace_ok, .error_widget_arrow.ace_ok{ border-color: #5aaa5a } .error_widget_arrow { position: absolute; border: solid 5px; border-top-color: transparent!important; border-right-color: transparent!important; border-left-color: transparent!important; top: -5px; }","")}),ace.define("ace/ace",["require","exports","module","ace/lib/fixoldbrowsers","ace/lib/dom","ace/lib/event","ace/range","ace/editor","ace/edit_session","ace/undomanager","ace/virtual_renderer","ace/worker/worker_client","ace/keyboard/hash_handler","ace/placeholder","ace/multi_select","ace/mode/folding/fold_mode","ace/theme/textmate","ace/ext/error_marker","ace/config"],function(e,t,n){"use strict";e("./lib/fixoldbrowsers");var r=e("./lib/dom"),i=e("./lib/event"),s=e("./range").Range,o=e("./editor").Editor,u=e("./edit_session").EditSession,a=e("./undomanager").UndoManager,f=e("./virtual_renderer").VirtualRenderer;e("./worker/worker_client"),e("./keyboard/hash_handler"),e("./placeholder"),e("./multi_select"),e("./mode/folding/fold_mode"),e("./theme/textmate"),e("./ext/error_marker"),t.config=e("./config"),t.require=e,typeof define=="function"&&(t.define=define),t.edit=function(e,n){if(typeof e=="string"){var s=e;e=document.getElementById(s);if(!e)throw new Error("ace.edit can't find div #"+s)}if(e&&e.env&&e.env.editor instanceof o)return e.env.editor;var u="";if(e&&/input|textarea/i.test(e.tagName)){var a=e;u=a.value,e=r.createElement("pre"),a.parentNode.replaceChild(e,a)}else e&&(u=e.textContent,e.innerHTML="");var l=t.createEditSession(u),c=new o(new f(e),l,n),h={document:l,editor:c,onResize:c.resize.bind(c,null)};return a&&(h.textarea=a),i.addListener(window,"resize",h.onResize),c.on("destroy",function(){i.removeListener(window,"resize",h.onResize),h.editor.container.env=null}),c.container.env=c.env=h,c},t.createEditSession=function(e,t){var n=new u(e,t);return n.setUndoManager(new a),n},t.Range=s,t.Editor=o,t.EditSession=u,t.UndoManager=a,t.VirtualRenderer=f,t.version="1.4.4"}); (function() { + ace.require(["ace/ace"], function(a) { + if (a) { + a.config.init(true); + a.define = ace.define; + } + if (!window.ace) + window.ace = a; + for (var key in a) if (a.hasOwnProperty(key)) + window.ace[key] = a[key]; + window.ace["default"] = window.ace; + if (typeof module == "object" && typeof exports == "object" && module) { + module.exports = window.ace; + } + }); + })(); diff --git a/ayu-highlight.css b/ayu-highlight.css new file mode 100644 index 0000000..32c9432 --- /dev/null +++ b/ayu-highlight.css @@ -0,0 +1,78 @@ +/* +Based off of the Ayu theme +Original by Dempfi (https://github.com/dempfi/ayu) +*/ + +.hljs { + display: block; + overflow-x: auto; + background: #191f26; + color: #e6e1cf; +} + +.hljs-comment, +.hljs-quote { + color: #5c6773; + font-style: italic; +} + +.hljs-variable, +.hljs-template-variable, +.hljs-attribute, +.hljs-attr, +.hljs-regexp, +.hljs-link, +.hljs-selector-id, +.hljs-selector-class { + color: #ff7733; +} + +.hljs-number, +.hljs-meta, +.hljs-builtin-name, +.hljs-literal, +.hljs-type, +.hljs-params { + color: #ffee99; +} + +.hljs-string, +.hljs-bullet { + color: #b8cc52; +} + +.hljs-title, +.hljs-built_in, +.hljs-section { + color: #ffb454; +} + +.hljs-keyword, +.hljs-selector-tag, +.hljs-symbol { + color: #ff7733; +} + +.hljs-name { + color: #36a3d9; +} + +.hljs-tag { + color: #00568d; +} + +.hljs-emphasis { + font-style: italic; +} + +.hljs-strong { + font-weight: bold; +} + +.hljs-addition { + color: #91b362; +} + +.hljs-deletion { + color: #d96c75; +} diff --git a/book.js b/book.js new file mode 100644 index 0000000..7f99e31 --- /dev/null +++ b/book.js @@ -0,0 +1,751 @@ +/* + This pull request seems to be stalled: + https://github.com/rust-lang/mdBook/pull/1759 + + So for now, we'll label Forge code as "rust" to enable the play button. +*/ + +"use strict"; + +// Fix back button cache problem +window.onunload = function () { }; + +// Global variable, shared between modules +function playground_text(playground, hidden = true) { + let code_block = playground.querySelector("code"); + + if (window.ace && code_block.classList.contains("editable")) { + let editor = window.ace.edit(code_block); + return editor.getValue(); + } else if (hidden) { + return code_block.textContent; + } else { + return code_block.innerText; + } +} + +(function codeSnippets() { + // Default to 10 seconds wait + function fetch_with_timeout(url, options, timeout = 10000) { + return Promise.race([ + fetch(url, options), + new Promise((_, reject) => setTimeout(() => reject(new Error('timeout')), timeout)) + ]); + } + + var playgrounds = Array.from(document.querySelectorAll(".playground")); + //console.log(playgrounds) + // TN: no crates to fetch etc.; just Forge + //playgrounds.forEach(block => handle_playground_update(block)); + + // if (playgrounds.length > 0) { + // fetch_with_timeout("https://play.rust-lang.org/meta/crates", { + // headers: { + // 'Content-Type': "application/json", + // }, + // method: 'POST', + // mode: 'cors', + // }) + // .then(response => response.json()) + // .then(response => { + // // get list of crates available in the rust playground + // let playground_crates = response.crates.map(item => item["id"]); + // playgrounds.forEach(block => handle_crate_list_update(block, playground_crates)); + // }); + // } + + // function handle_crate_list_update(playground_block, playground_crates) { + // // update the play buttons after receiving the response + // update_play_button(playground_block, playground_crates); + + // // and install on change listener to dynamically update ACE editors + // if (window.ace) { + // let code_block = playground_block.querySelector("code"); + // if (code_block.classList.contains("editable")) { + // let editor = window.ace.edit(code_block); + // editor.addEventListener("change", function (e) { + // update_play_button(playground_block, playground_crates); + // }); + // // add Ctrl-Enter command to execute rust code + // editor.commands.addCommand({ + // name: "run", + // bindKey: { + // win: "Ctrl-Enter", + // mac: "Ctrl-Enter" + // }, + // exec: _editor => run_rust_code(playground_block) + // }); + // } + // } + // } + + // function handle_playground_update(playground_block) { + // // update the play buttons after receiving the response + // update_play_button(playground_block); + + // // and install on change listener to dynamically update ACE editors + // if (window.ace) { + // let code_block = playground_block.querySelector("code"); + // if (code_block.classList.contains("editable")) { + // let editor = window.ace.edit(code_block); + // editor.addEventListener("change", function (e) { + // update_play_button(playground_block); + // }); + // // add Ctrl-Enter command to execute rust code + // editor.commands.addCommand({ + // name: "run", + // bindKey: { + // win: "Ctrl-Enter", + // mac: "Ctrl-Enter" + // }, + // exec: _editor => run_rust_code(playground_block) + // }); + // } + // } + // } + + // // updates the visibility of play button based on `no_run` class and + // // used crates vs ones available on https://play.rust-lang.org + // function update_play_button(pre_block) { + // var play_button = pre_block.querySelector(".play-button"); + + // // skip if code is `no_run` + // if (pre_block.querySelector('code').classList.contains("no_run")) { + // play_button.classList.add("hidden"); + // return; + // } + + // // // get list of `extern crate`'s from snippet + // // var txt = playground_text(pre_block); + // // var re = /extern\s+crate\s+([a-zA-Z_0-9]+)\s*;/g; + // // var snippet_crates = []; + // // var item; + // // while (item = re.exec(txt)) { + // // snippet_crates.push(item[1]); + // // } + + // // // check if all used crates are available on play.rust-lang.org + // // var all_available = snippet_crates.every(function (elem) { + // // return playground_crates.indexOf(elem) > -1; + // // }); + + // // if (all_available) { + // play_button.classList.remove("hidden"); + // // } else { + // // play_button.classList.add("hidden"); + // // } + // } + + function run_rust_code(code_block) { + var result_block = code_block.querySelector(".result"); + if (!result_block) { + result_block = document.createElement('code'); + result_block.className = 'result hljs language-bash'; + + code_block.append(result_block); + } + + let text = playground_text(code_block); + //let classes = code_block.querySelector('code').classList; + // let edition = "2015"; + // if(classes.contains("edition2018")) { + // edition = "2018"; + // } else if(classes.contains("edition2021")) { + // edition = "2021"; + // } + // var params = { + // //version: "stable", + // //optimize: "0", + // code: text, + // //edition: edition + // }; + + // if (text.indexOf("#![feature") !== -1) { + // params.version = "nightly"; + // } + + result_block.innerText = "Running..."; + console.log(text) + // TN: edit here; localhost + also not http*S* + // TN: TODO: server not expecting JSON maybe? (but why would it say #f?) + fetch_with_timeout("http://localhost:17100/load", { + headers: { + // TN: avoid pre-flighting, since OPTIONS requests not supported by default in racket webserver + //'Content-Type': "application/json", + 'Content-Type': 'text/plain', + // TN: declare the client understands JSON + 'Accept': "application/json" + }, + method: 'POST', + // This prevents anything other than HEAD/GET/POST, prevent non-simple headers + // but remove the obligation for the server to send Access-Control-Allow-Origin + // which would be OK, except it also prevents the front-end script from + // seeing the response data. So we need to use CORS and headers. + //mode: 'no-cors', + mode: 'cors', + body: text // JSON.stringify(params) + }) + .then(response => response.json()) + .then(response => { + // This file is now loaded on the Forge service + // Are there any run commands to run? + if(response.run_ids.length !== 1) { + result_block.innerText = `Response contained ${response.run_ids.length} commands; auto-run requires a single command only.`; + result_block.classList.add("result-no-output"); + } + const id = response.run_ids[0] + fetch_with_timeout(`http://localhost:17100/next?id=${id}`, { + headers: { + 'Content-Type': 'text/plain', + 'Accept': "application/json" + }, + method: 'GET', + mode: 'cors', + }) + .then(response => response.json()) + .then(response => { + result_block.innerText = response.instance; + result_block.classList.remove("result-no-output"); + }) + // if (response.result.trim() === '') { + // result_block.innerText = "No output"; + // result_block.classList.add("result-no-output"); + // } else { + // result_block.innerText = response.result; + // result_block.classList.remove("result-no-output"); + // } + }) + .catch(error => result_block.innerText = "Error communicating with Forge service: " + error.message); + } + + // Syntax highlighting Configuration + hljs.configure({ + tabReplace: ' ', // 4 spaces + languages: [], // Languages used for auto-detection + }); + + let code_nodes = Array + .from(document.querySelectorAll('code')) + // Don't highlight `inline code` blocks in headers. + .filter(function (node) {return !node.parentElement.classList.contains("header"); }); + + if (window.ace) { + // language-rust class needs to be removed for editable + // blocks or highlightjs will capture events + code_nodes + .filter(function (node) {return node.classList.contains("editable"); }) + .forEach(function (block) { block.classList.remove('language-rust'); }); + + code_nodes + .filter(function (node) {return !node.classList.contains("editable"); }) + .forEach(function (block) { hljs.highlightBlock(block); }); + } else { + code_nodes.forEach(function (block) { hljs.highlightBlock(block); }); + } + + // Adding the hljs class gives code blocks the color css + // even if highlighting doesn't apply + code_nodes.forEach(function (block) { block.classList.add('hljs'); }); + + Array.from(document.querySelectorAll("code.hljs")).forEach(function (block) { + + var lines = Array.from(block.querySelectorAll('.boring')); + // If no lines were hidden, return + if (!lines.length) { return; } + block.classList.add("hide-boring"); + + var buttons = document.createElement('div'); + buttons.className = 'buttons'; + buttons.innerHTML = ""; + + // add expand button + var pre_block = block.parentNode; + pre_block.insertBefore(buttons, pre_block.firstChild); + + pre_block.querySelector('.buttons').addEventListener('click', function (e) { + if (e.target.classList.contains('fa-eye')) { + e.target.classList.remove('fa-eye'); + e.target.classList.add('fa-eye-slash'); + e.target.title = 'Hide lines'; + e.target.setAttribute('aria-label', e.target.title); + + block.classList.remove('hide-boring'); + } else if (e.target.classList.contains('fa-eye-slash')) { + e.target.classList.remove('fa-eye-slash'); + e.target.classList.add('fa-eye'); + e.target.title = 'Show hidden lines'; + e.target.setAttribute('aria-label', e.target.title); + + block.classList.add('hide-boring'); + } + }); + }); + + if (window.playground_copyable) { + Array.from(document.querySelectorAll('pre code')).forEach(function (block) { + var pre_block = block.parentNode; + if (!pre_block.classList.contains('playground')) { + var buttons = pre_block.querySelector(".buttons"); + if (!buttons) { + buttons = document.createElement('div'); + buttons.className = 'buttons'; + pre_block.insertBefore(buttons, pre_block.firstChild); + } + + var clipButton = document.createElement('button'); + clipButton.className = 'fa fa-copy clip-button'; + clipButton.title = 'Copy to clipboard'; + clipButton.setAttribute('aria-label', clipButton.title); + clipButton.innerHTML = ''; + + buttons.insertBefore(clipButton, buttons.firstChild); + } + }); + } + + // Process playground code blocks + Array.from(document.querySelectorAll(".playground")).forEach(function (pre_block) { + + // Add play button + var buttons = pre_block.querySelector(".buttons"); + if (!buttons) { + buttons = document.createElement('div'); + buttons.className = 'buttons'; + pre_block.insertBefore(buttons, pre_block.firstChild); + } + + var runCodeButton = document.createElement('button'); + runCodeButton.className = 'fa fa-play play-button'; + runCodeButton.hidden = true; + runCodeButton.title = 'Run this code'; + runCodeButton.setAttribute('aria-label', runCodeButton.title); + + buttons.insertBefore(runCodeButton, buttons.firstChild); + runCodeButton.addEventListener('click', function (e) { + run_rust_code(pre_block); + }); + + if (window.playground_copyable) { + var copyCodeClipboardButton = document.createElement('button'); + copyCodeClipboardButton.className = 'fa fa-copy clip-button'; + copyCodeClipboardButton.innerHTML = ''; + copyCodeClipboardButton.title = 'Copy to clipboard'; + copyCodeClipboardButton.setAttribute('aria-label', copyCodeClipboardButton.title); + + buttons.insertBefore(copyCodeClipboardButton, buttons.firstChild); + } + + let code_block = pre_block.querySelector("code"); + if (window.ace && code_block.classList.contains("editable")) { + var undoChangesButton = document.createElement('button'); + undoChangesButton.className = 'fa fa-history reset-button'; + undoChangesButton.title = 'Undo changes'; + undoChangesButton.setAttribute('aria-label', undoChangesButton.title); + + buttons.insertBefore(undoChangesButton, buttons.firstChild); + + undoChangesButton.addEventListener('click', function () { + let editor = window.ace.edit(code_block); + editor.setValue(editor.originalCode); + editor.clearSelection(); + }); + } + }); +})(); + +(function themes() { + var html = document.querySelector('html'); + var themeToggleButton = document.getElementById('theme-toggle'); + var themePopup = document.getElementById('theme-list'); + var themeColorMetaTag = document.querySelector('meta[name="theme-color"]'); + var stylesheets = { + ayuHighlight: document.querySelector("[href$='ayu-highlight.css']"), + tomorrowNight: document.querySelector("[href$='tomorrow-night.css']"), + highlight: document.querySelector("[href$='highlight.css']"), + }; + + function showThemes() { + themePopup.style.display = 'block'; + themeToggleButton.setAttribute('aria-expanded', true); + themePopup.querySelector("button#" + get_theme()).focus(); + } + + function updateThemeSelected() { + themePopup.querySelectorAll('.theme-selected').forEach(function (el) { + el.classList.remove('theme-selected'); + }); + themePopup.querySelector("button#" + get_theme()).classList.add('theme-selected'); + } + + function hideThemes() { + themePopup.style.display = 'none'; + themeToggleButton.setAttribute('aria-expanded', false); + themeToggleButton.focus(); + } + + function get_theme() { + var theme; + try { theme = localStorage.getItem('mdbook-theme'); } catch (e) { } + if (theme === null || theme === undefined) { + return default_theme; + } else { + return theme; + } + } + + function set_theme(theme, store = true) { + let ace_theme; + + if (theme == 'coal' || theme == 'navy') { + stylesheets.ayuHighlight.disabled = true; + stylesheets.tomorrowNight.disabled = false; + stylesheets.highlight.disabled = true; + + ace_theme = "ace/theme/tomorrow_night"; + } else if (theme == 'ayu') { + stylesheets.ayuHighlight.disabled = false; + stylesheets.tomorrowNight.disabled = true; + stylesheets.highlight.disabled = true; + ace_theme = "ace/theme/tomorrow_night"; + } else { + stylesheets.ayuHighlight.disabled = true; + stylesheets.tomorrowNight.disabled = true; + stylesheets.highlight.disabled = false; + ace_theme = "ace/theme/dawn"; + } + + setTimeout(function () { + themeColorMetaTag.content = getComputedStyle(document.body).backgroundColor; + }, 1); + + if (window.ace && window.editors) { + window.editors.forEach(function (editor) { + editor.setTheme(ace_theme); + }); + } + + var previousTheme = get_theme(); + + if (store) { + try { localStorage.setItem('mdbook-theme', theme); } catch (e) { } + } + + html.classList.remove(previousTheme); + html.classList.add(theme); + updateThemeSelected(); + } + + // Set theme + var theme = get_theme(); + + set_theme(theme, false); + + themeToggleButton.addEventListener('click', function () { + if (themePopup.style.display === 'block') { + hideThemes(); + } else { + showThemes(); + } + }); + + themePopup.addEventListener('click', function (e) { + var theme; + if (e.target.className === "theme") { + theme = e.target.id; + } else if (e.target.parentElement.className === "theme") { + theme = e.target.parentElement.id; + } else { + return; + } + set_theme(theme); + }); + + themePopup.addEventListener('focusout', function(e) { + // e.relatedTarget is null in Safari and Firefox on macOS (see workaround below) + if (!!e.relatedTarget && !themeToggleButton.contains(e.relatedTarget) && !themePopup.contains(e.relatedTarget)) { + hideThemes(); + } + }); + + // Should not be needed, but it works around an issue on macOS & iOS: https://github.com/rust-lang/mdBook/issues/628 + document.addEventListener('click', function(e) { + if (themePopup.style.display === 'block' && !themeToggleButton.contains(e.target) && !themePopup.contains(e.target)) { + hideThemes(); + } + }); + + document.addEventListener('keydown', function (e) { + if (e.altKey || e.ctrlKey || e.metaKey || e.shiftKey) { return; } + if (!themePopup.contains(e.target)) { return; } + + switch (e.key) { + case 'Escape': + e.preventDefault(); + hideThemes(); + break; + case 'ArrowUp': + e.preventDefault(); + var li = document.activeElement.parentElement; + if (li && li.previousElementSibling) { + li.previousElementSibling.querySelector('button').focus(); + } + break; + case 'ArrowDown': + e.preventDefault(); + var li = document.activeElement.parentElement; + if (li && li.nextElementSibling) { + li.nextElementSibling.querySelector('button').focus(); + } + break; + case 'Home': + e.preventDefault(); + themePopup.querySelector('li:first-child button').focus(); + break; + case 'End': + e.preventDefault(); + themePopup.querySelector('li:last-child button').focus(); + break; + } + }); +})(); + +(function sidebar() { + var html = document.querySelector("html"); + var sidebar = document.getElementById("sidebar"); + var sidebarLinks = document.querySelectorAll('#sidebar a'); + var sidebarToggleButton = document.getElementById("sidebar-toggle"); + var sidebarResizeHandle = document.getElementById("sidebar-resize-handle"); + var firstContact = null; + + function showSidebar() { + html.classList.remove('sidebar-hidden') + html.classList.add('sidebar-visible'); + Array.from(sidebarLinks).forEach(function (link) { + link.setAttribute('tabIndex', 0); + }); + sidebarToggleButton.setAttribute('aria-expanded', true); + sidebar.setAttribute('aria-hidden', false); + try { localStorage.setItem('mdbook-sidebar', 'visible'); } catch (e) { } + } + + + var sidebarAnchorToggles = document.querySelectorAll('#sidebar a.toggle'); + + function toggleSection(ev) { + ev.currentTarget.parentElement.classList.toggle('expanded'); + } + + Array.from(sidebarAnchorToggles).forEach(function (el) { + el.addEventListener('click', toggleSection); + }); + + function hideSidebar() { + html.classList.remove('sidebar-visible') + html.classList.add('sidebar-hidden'); + Array.from(sidebarLinks).forEach(function (link) { + link.setAttribute('tabIndex', -1); + }); + sidebarToggleButton.setAttribute('aria-expanded', false); + sidebar.setAttribute('aria-hidden', true); + try { localStorage.setItem('mdbook-sidebar', 'hidden'); } catch (e) { } + } + + // Toggle sidebar + sidebarToggleButton.addEventListener('click', function sidebarToggle() { + if (html.classList.contains("sidebar-hidden")) { + var current_width = parseInt( + document.documentElement.style.getPropertyValue('--sidebar-width'), 10); + if (current_width < 150) { + document.documentElement.style.setProperty('--sidebar-width', '150px'); + } + showSidebar(); + } else if (html.classList.contains("sidebar-visible")) { + hideSidebar(); + } else { + if (getComputedStyle(sidebar)['transform'] === 'none') { + hideSidebar(); + } else { + showSidebar(); + } + } + }); + + sidebarResizeHandle.addEventListener('mousedown', initResize, false); + + function initResize(e) { + window.addEventListener('mousemove', resize, false); + window.addEventListener('mouseup', stopResize, false); + html.classList.add('sidebar-resizing'); + } + function resize(e) { + var pos = (e.clientX - sidebar.offsetLeft); + if (pos < 20) { + hideSidebar(); + } else { + if (html.classList.contains("sidebar-hidden")) { + showSidebar(); + } + pos = Math.min(pos, window.innerWidth - 100); + document.documentElement.style.setProperty('--sidebar-width', pos + 'px'); + } + } + //on mouseup remove windows functions mousemove & mouseup + function stopResize(e) { + html.classList.remove('sidebar-resizing'); + window.removeEventListener('mousemove', resize, false); + window.removeEventListener('mouseup', stopResize, false); + } + + document.addEventListener('touchstart', function (e) { + firstContact = { + x: e.touches[0].clientX, + time: Date.now() + }; + }, { passive: true }); + + document.addEventListener('touchmove', function (e) { + if (!firstContact) + return; + + var curX = e.touches[0].clientX; + var xDiff = curX - firstContact.x, + tDiff = Date.now() - firstContact.time; + + if (tDiff < 250 && Math.abs(xDiff) >= 150) { + if (xDiff >= 0 && firstContact.x < Math.min(document.body.clientWidth * 0.25, 300)) + showSidebar(); + else if (xDiff < 0 && curX < 300) + hideSidebar(); + + firstContact = null; + } + }, { passive: true }); +})(); + +(function chapterNavigation() { + document.addEventListener('keydown', function (e) { + if (e.altKey || e.ctrlKey || e.metaKey || e.shiftKey) { return; } + if (window.search && window.search.hasFocus()) { return; } + + switch (e.key) { + case 'ArrowRight': + e.preventDefault(); + var nextButton = document.querySelector('.nav-chapters.next'); + if (nextButton) { + window.location.href = nextButton.href; + } + break; + case 'ArrowLeft': + e.preventDefault(); + var previousButton = document.querySelector('.nav-chapters.previous'); + if (previousButton) { + window.location.href = previousButton.href; + } + break; + } + }); +})(); + +(function clipboard() { + var clipButtons = document.querySelectorAll('.clip-button'); + + function hideTooltip(elem) { + elem.firstChild.innerText = ""; + elem.className = 'fa fa-copy clip-button'; + } + + function showTooltip(elem, msg) { + elem.firstChild.innerText = msg; + elem.className = 'fa fa-copy tooltipped'; + } + + var clipboardSnippets = new ClipboardJS('.clip-button', { + text: function (trigger) { + hideTooltip(trigger); + let playground = trigger.closest("pre"); + return playground_text(playground, false); + } + }); + + Array.from(clipButtons).forEach(function (clipButton) { + clipButton.addEventListener('mouseout', function (e) { + hideTooltip(e.currentTarget); + }); + }); + + clipboardSnippets.on('success', function (e) { + e.clearSelection(); + showTooltip(e.trigger, "Copied!"); + }); + + clipboardSnippets.on('error', function (e) { + showTooltip(e.trigger, "Clipboard error!"); + }); +})(); + +(function scrollToTop () { + var menuTitle = document.querySelector('.menu-title'); + + menuTitle.addEventListener('click', function () { + document.scrollingElement.scrollTo({ top: 0, behavior: 'smooth' }); + }); +})(); + +(function controllMenu() { + var menu = document.getElementById('menu-bar'); + + (function controllPosition() { + var scrollTop = document.scrollingElement.scrollTop; + var prevScrollTop = scrollTop; + var minMenuY = -menu.clientHeight - 50; + // When the script loads, the page can be at any scroll (e.g. if you reforesh it). + menu.style.top = scrollTop + 'px'; + // Same as parseInt(menu.style.top.slice(0, -2), but faster + var topCache = menu.style.top.slice(0, -2); + menu.classList.remove('sticky'); + var stickyCache = false; // Same as menu.classList.contains('sticky'), but faster + document.addEventListener('scroll', function () { + scrollTop = Math.max(document.scrollingElement.scrollTop, 0); + // `null` means that it doesn't need to be updated + var nextSticky = null; + var nextTop = null; + var scrollDown = scrollTop > prevScrollTop; + var menuPosAbsoluteY = topCache - scrollTop; + if (scrollDown) { + nextSticky = false; + if (menuPosAbsoluteY > 0) { + nextTop = prevScrollTop; + } + } else { + if (menuPosAbsoluteY > 0) { + nextSticky = true; + } else if (menuPosAbsoluteY < minMenuY) { + nextTop = prevScrollTop + minMenuY; + } + } + if (nextSticky === true && stickyCache === false) { + menu.classList.add('sticky'); + stickyCache = true; + } else if (nextSticky === false && stickyCache === true) { + menu.classList.remove('sticky'); + stickyCache = false; + } + if (nextTop !== null) { + menu.style.top = nextTop + 'px'; + topCache = nextTop; + } + prevScrollTop = scrollTop; + }, { passive: true }); + })(); + (function controllBorder() { + function updateBorder() { + if (menu.offsetTop === 0) { + menu.classList.remove('bordered'); + } else { + menu.classList.add('bordered'); + } + } + updateBorder(); + document.addEventListener('scroll', updateBorder, { passive: true }); + })(); +})(); diff --git a/chapters/bst/bst.html b/chapters/bst/bst.html new file mode 100644 index 0000000..d066c42 --- /dev/null +++ b/chapters/bst/bst.html @@ -0,0 +1,301 @@ + + + + + +
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/chapters/manifesto/borrow-newt-custom.png b/chapters/manifesto/borrow-newt-custom.png
new file mode 100644
index 0000000..596bc44
Binary files /dev/null and b/chapters/manifesto/borrow-newt-custom.png differ
diff --git a/chapters/manifesto/manifesto.html b/chapters/manifesto/manifesto.html
new file mode 100644
index 0000000..1dceb2a
--- /dev/null
+++ b/chapters/manifesto/manifesto.html
@@ -0,0 +1,385 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Intro to Modeling Systems (Part 2: BSTs)
+Now that we've written our first model—tic-tac-toe boards—let's switch to something a bit more serious: binary search trees. A binary search tree (BST) with an added property about its structure. So let's start modeling by following the our 5-step process.
+Datatypes
+A binary tree is made up of nodes:
+#lang forge/froglet
+sig Node {
+ key: one Int, -- every node has some key
+ left: lone Node, -- every node has at most one left-child
+ right: lone Node -- every node has at most one right-child
+}
+Wellformedness
+What makes a binary tree a binary tree? One way to say it is:
+-
+
- it's tree-shaped: there are no cycles and nodes have at most one parent node; and +
- it's connected, that is, it's a tree and not a forest. +
Let's get started encoding this. Sometimes it can be helpful to write a domain predicate along with wellformedness, if it makes the model more clear, hence why we wrote root:
#lang forge/froglet
+sig Node {
+ key: one Int, -- every node has some key
+ left: lone Node, -- every node has at most one left-child
+ right: lone Node -- every node has at most one right-child
+}
+
+pred root[n: Node] {
+ -- a node is a root if it has no ancestor (note this doesn't enforce uniqueness)
+ no n2: Node | n = n2.left or n = n2.right
+}
+
+pred wellformed {
+ -- no cycles: no node can reach itself via a succession of left and right fields
+ all n: Node | not reachable[n, n, left, right]
+
+ -- all non-root nodes have a common ancestor from which both are reachable
+ -- the "disj" keyword means that n1 and n2 must be _different_
+ all disj n1, n2: Node | (not root[n1] and not root[n2]) implies {
+ some anc: Node | reachable[n1, anc, left, right] and
+ reachable[n2, anc, left, right] }
+
+ -- nodes have a unique parent (if any)
+ all disj n1, n2, n3: Node |
+ not ((n1.left = n3 or n1.right = n3) and (n2.left = n3 or n2.right = n3))
+
+}
+Write an example or two
+[FILL: example trees: singleton, empty, unbalanced...]
+View some instances
+-- View a tree or two
+run {binary_tree} for exactly 8 Node
+[FILL: Oops, not quite right, we were missing a constraint; underconstraint bug -- fix it]
+Missing:
+ -- left+right differ (unless both are empty)
+ all n: Node | some n.left => n.left != n.right
+FILL: and iterate.
+Going further
+-- Run a test: our predicate enforces a unique root exists (if any node exists)
+pred req_unique_root {
+ no Node or {
+ one root: Node |
+ all other: Node-root | other in descendantsOf[root]}}
+assert binary_tree is sufficient for req_unique_root for 5 Node
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/chapters/manifesto/netlab-custom-def1.png b/chapters/manifesto/netlab-custom-def1.png
new file mode 100644
index 0000000..1f4fe5c
Binary files /dev/null and b/chapters/manifesto/netlab-custom-def1.png differ
diff --git a/chapters/manifesto/ns-custom.png b/chapters/manifesto/ns-custom.png
new file mode 100644
index 0000000..9f9a331
Binary files /dev/null and b/chapters/manifesto/ns-custom.png differ
diff --git a/chapters/manifesto/reflect-0-custom.png b/chapters/manifesto/reflect-0-custom.png
new file mode 100644
index 0000000..25d9dce
Binary files /dev/null and b/chapters/manifesto/reflect-0-custom.png differ
diff --git a/chapters/manifesto/spikeball.png b/chapters/manifesto/spikeball.png
new file mode 100644
index 0000000..bbd338e
Binary files /dev/null and b/chapters/manifesto/spikeball.png differ
diff --git a/chapters/manifesto/texas.png b/chapters/manifesto/texas.png
new file mode 100644
index 0000000..8a63104
Binary files /dev/null and b/chapters/manifesto/texas.png differ
diff --git a/chapters/manifesto/triple-triad.png b/chapters/manifesto/triple-triad.png
new file mode 100644
index 0000000..b1238b1
Binary files /dev/null and b/chapters/manifesto/triple-triad.png differ
diff --git a/chapters/manifesto/uno.png b/chapters/manifesto/uno.png
new file mode 100644
index 0000000..5c22ef3
Binary files /dev/null and b/chapters/manifesto/uno.png differ
diff --git a/chapters/ttt/ttt-custom.png b/chapters/ttt/ttt-custom.png
new file mode 100644
index 0000000..2e704e3
Binary files /dev/null and b/chapters/ttt/ttt-custom.png differ
diff --git a/chapters/ttt/ttt-viz-table.png b/chapters/ttt/ttt-viz-table.png
new file mode 100644
index 0000000..3a920d4
Binary files /dev/null and b/chapters/ttt/ttt-viz-table.png differ
diff --git a/chapters/ttt/ttt-viz.png b/chapters/ttt/ttt-viz.png
new file mode 100644
index 0000000..cf080ce
Binary files /dev/null and b/chapters/ttt/ttt-viz.png differ
diff --git a/chapters/ttt/ttt.html b/chapters/ttt/ttt.html
new file mode 100644
index 0000000..2b5df49
--- /dev/null
+++ b/chapters/ttt/ttt.html
@@ -0,0 +1,609 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Logic for Systems
+Setting the Stage
+If you're taking this course or reading this book, you've probably had to complete some programming assignments---or at least written some small program for a course or an online tutorial. Take a moment to list a handful of such assignments: what did you have to build?
+Now ask yourself:
+-
+
- How did you know what behavior to implement? +
- How did you know which data structures or algorithms were the right ones to use? +
- How did you know your program "worked", in the end? +
In the context of a course, there are "expected" answers to these questions. For instance, you might say you know your code worked because you tested it (very thoroughly)! But is that really the truth? In terms of consequences, the true bar for excellent in a programming class is the grade you got. That is:
+-
+
- You knew what to do because you were told what to do. +
- You probably knew which algorithms to use because they'd just been taught to you. +
- You were confident that your programs worked because you were told by an authority figure. +
But outside that context, as (say) a professional engineer, you lose the safety net. You might be working on a program that controls the fate of billions of dollars, tempers geopolitical strife, or controls a patient's insulin pump. Even if you had a TA, would you trust them to tell you that those programs worked? Would you trust your boss to understand exactly what needed to happen, and tell you exactly how to do it? Probably not! Instead, you need to think carefully about what you want, how to build it, and how to evaluate what you and others have built.
+
+
+
+
+
+As engineers, we strive for perfection. But perfection is an ideal; it's not obtainable. Why? First: we're human. Even if we could read our customers' minds, that's no guarantee that they know what they really need. And even if we can prove our code is correct, we might be checking for the wrong things. Second: our environment is hostile. Computers break. Patches to dependencies introduce errors. Cosmic radiation can flip bits in memory. 100% reliability is hopeless. Anyone who tells you differently is trying to sell you something.
+But that doesn't mean we should give up. It just means that we should moderate our expectations. This book won't teach you how to never make mistakes. Instead, it will teach you a multiple ways to increase your confidence in correctness.
+Unit Testing
+Let's start with unit-testing and deconstruct it. What does it do well? What does it do poorly?
+Exercise: Make two lists to answer the above question. Why do we test? What could go wrong, and how can the sort of testing you've done in other classes let us down?
+Hopefully we all agree that concrete input-output testing has its virtues and that we should keep doing it. But let's focus on the things that testing doesn't do well.
+
+
+Think, then click!
+You might have observed that (for most interesting programs, anyway) tests cannot be exhaustive because there are infinitely many possible inputs. And since we're forced to test non-exhaustively, we have to hope we pick good tests---tests that not only focus on our own implementation, but on others (like the implementation that replaces yours eventually) too.
+Worse, we can't test the things we don't think of, or don't know about; we're vulnerable to our limited knowledge, the availability heuristic, confirmation bias, and so on. In fact, we humans are generally ill equipped for logical reasoning, even if trained.
+Humans and Reasoning
+A Toy Example
+Suppose we're thinking about the workings of a small company. We're given some facts about the company, and have to answer a question based on those facts. Here's an example. We know that:
+-
+
- Alice supervises Bob. +
- Bob supervises Charlie. +
- Alice graduated Brown. +
- Charlie graduated Harvale. +
Question: Does someone who graduated from Brown directly supervise someone who graduated from another University?
+
+
+Think, then click.
+Yes! Regardless of whether Bob graduated from Brown, some Brown graduate supervises some non-Brown graduate. Reasoning by hypotheticals, there is one fact we don't know: where Bob graduated. In case he graduated Brown, he supervises Charlie, a non-Brown graduate. In case he graduated from another school, he's supervised by Alice, a Brown graduate.
+Humans tend to be very bad at reasoning by hypotheticals. There's a temptation to think that this puzzle isn't solvable because we don't know where Bob graduated from. Even Tim thought this at first after seeing the puzzle—in grad school! For logic!
+Now imagine a puzzle with a thousand of these unknowns. A thousand boolean variables means cases to reason through. Want to use a computer yet?
+ +Of course, this isn't really about logic puzzles.
+A Real Scenario
+There's a real cryptographic protocol called the Needham-Schroeder public-key protocol. You can read about it here. Unfortunately the protocol has a bug: it's vulnerable to attack if one of the principles can be fooled into starting an exchange with a badly-behaved or compromised agent. We won't go into specifics. Instead, let's focus on the fact that it's quite easy to get things like protocols wrong, and sometimes challenging for us humans to completely explore all possible behaviors -- especially since there might be behaviors we'd never even considered! It sure would be nice if we could get a computer to help out with that.
+A pair of former 1710 students did an ISP on modeling crypto protocols, using the tools you'll learn in class. Here's an example picture, generated by their model, of the flaw in the Needham-Schroeder protocol:
+
You don't need to understand the specifics of the visualization; the point is that someone who has studied crypto protocols would. And this really does show the classic attack on Needham-Schroeder. You may not be a crypto-protocol person, but you probably are an expert in something you'd like to model, and you might very well get the chance to do so this semester.
+Automated Reasoning as an Assistive Device
+The human species has been so successful, in part, because of our ability to use assistive devices—tools! Eyeglasses, bicycles, hammers, bridges: all devices that assist us in navigating the world in our fragile meat-bodies. One of our oldest inventions, writing, is an assistive device that increases our long-term memory space and makes that memory persistent. Computers are only one in a long line of such inventions.
+So, naturally, we've found ways to:
+-
+
- use computers to help us test our ideas; +
- use computers to exhaustively check program correctness; +
- use computers to help us find gaps in our intuition about a program; +
- use computers to help us explore the design space of a data structure, or algorithm, card game, or chemical reaction; +
- etc. +
There's a large body of work in Computer Science that uses logic to do all those things. We tend to call it formal methods, especially when the focus is on reasoning about systems. It touches on topics like system modeling, constraint solving, program analysis, design exploration, and more. That's what this book is about: the foundational knowledge to engage with many different applications of these ideas, even if you don't end up working with them directly every day.
+More concretely, we'll focus on a class of techniques called lightweight formal methods, which are characterized by tradeoffs that favor ease of use over strong guarantees (although we'll sometimes achieve those as well).
+
+
+
+
+
+Jeanette Wing and Daniel Jackson wrote a short article coining the term "lightweight FM" in the 90's, which you can find online.
+
+
+
+
+
+When we say "systems" in this book we don't necessarily mean the kind of systems you see in a class on networks, hardware architecture, or operating systems. You can apply the techniques in this book to those subjects quite naturally, but you can also apply it to user interfaces, type systems in programming, hardware, version control systems like Git, web security, cryptographic protocols, robotics, puzzles, sports and games, and much more. So we construe the word "system" very broadly.
+Here are some examples of "systems" that students have modeled in Forge: lifetimes in Rust, network reachability, and poker!
+The Future of Computing
+For better or worse, The shape of engineering is changing. Lots of people are excited, scared, or both about large language models like ChatGPT. This book won't teach you how to use generative AI, so it's reasonable to wonder: why learn from this book, instead of another AI book?
+There are two questions that will never go out of style, and won't be answered by AI (at least, not in our lifetimes):
+-
+
- What do you want to build? What does your customer really need? Answering this requires talking to them and other stakeholders, watching their processes, seeking their feedback, and adjusting your design based on it. And no matter who (or what) is writing the actual code, you need to be able to express all this precisely enough that they (or it) can succeed at the implementation. +
- How will you evaluate what you get? No matter who (or what) is building the system, verification is needed before the system can be trusted. +
Even setting aside the customer-facing aspects, we'll still need to think critically about what it is we want and how to evaluate whether we're getting it. The skills you learn here will remain useful (or become even more so) as engineering evolves. And those skills will be useful for more than just code.
+ + +Looking Ahead: Tools
+The main tool we'll use in this course is Forge. Forge is a tool for modeling systems; we'll talk about what that means later on. For now, be aware that we'll be progressing through three language levels in Forge:
+-
+
- Froglet, which restricts the set of operations available so that we can jump right in more easily. If you have intuitions about object-oriented programming, those intuitions will be useful in Froglet, although there are a few important differences that we'll talk about. +
- Relational Forge, which expands the set of operations available to include sets, relations, and relational operators. Again, we'll cover these in detail later. They are useful for reasoning about complex relationships between objects and for representing certain domains, like databases or graphs. +
- Temporal Forge, which lets us cleanly model how a system's state evolves over time. +
We'll also use:
+-
+
- Hypothesis, a testing library for Python; and +
- Z3, an SMT solver library. +
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/chapters/ttt/ttt.js b/chapters/ttt/ttt.js
new file mode 100644
index 0000000..3d85f88
--- /dev/null
+++ b/chapters/ttt/ttt.js
@@ -0,0 +1,55 @@
+const d3 = require('d3')
+d3.selectAll("svg > *").remove();
+
+/*
+ Visualizer for the in-class tic-tac-toe model. This is written in "raw"
+ D3, rather than using our helper libraries. If you're familiar with
+ visualization in JavaScript using this popular library, this is how you
+ would use it with Forge.
+
+ Note that if you _aren't_ familiar, that's OK; we'll show more examples
+ and give more guidance in the near future. The helper library also makes
+ things rather easier.
+
+ TN 2024
+
+ Note: if you're using this style, the require for d3 needs to come before anything
+ else, even comments.
+*/
+
+function printValue(row, col, yoffset, value) {
+ d3.select(svg)
+ .append("text")
+ .style("fill", "black")
+ .attr("x", (row+1)*10)
+ .attr("y", (col+1)*14 + yoffset)
+ .text(value);
+}
+
+function printState(stateAtom, yoffset) {
+ for (r = 0; r <= 2; r++) {
+ for (c = 0; c <= 2; c++) {
+ printValue(r, c, yoffset,
+ stateAtom.board[r][c]
+ .toString().substring(0,1))
+ }
+ }
+
+ d3.select(svg)
+ .append('rect')
+ .attr('x', 5)
+ .attr('y', yoffset+1)
+ .attr('width', 40)
+ .attr('height', 50)
+ .attr('stroke-width', 2)
+ .attr('stroke', 'black')
+ .attr('fill', 'transparent');
+}
+
+
+var offset = 0
+for(b = 0; b <= 10; b++) {
+ if(Board.atom("Board"+b) != null)
+ printState(Board.atom("Board"+b), offset)
+ offset = offset + 55
+}
\ No newline at end of file
diff --git a/chapters/ttt/ttt_games.html b/chapters/ttt/ttt_games.html
new file mode 100644
index 0000000..b09fdc8
--- /dev/null
+++ b/chapters/ttt/ttt_games.html
@@ -0,0 +1,519 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Practice with
+
+
+
+
+ Intro to Modeling Systems (Part 1: Tic-Tac-Toe)
+What's a Model?
+A model is a representation of a system that faithfully includes some but not all of the system's complexity. There are many different ways to model a system, all of which have different advantages and disadvantages. Think about what a car company does before it produces a new car design. Among other things, it creates multiple models. E.g.,
+-
+
- it models the car in some computer-aided design tool; and then +
- creates a physical model of the car, perhaps with clay, for testing in wind tunnels etc. +
There may be many different models of a system, all of them focused on something different. As the statisticians say, "all models are wrong, but some models are useful". Learning how to model a system is a key skill for engineers, not just within "formal methods". Abstraction is one of the key tools in Computer Science, and modeling lies at the heart of abstraction.
+In this course, the models we build aren't inert; we have tools that we can use the explore and analyze them!
+Don't Be Afraid of Imperfect Representations
+We don't need to fully model a system to be able to make useful inferences. We can simplify, omit, and abstract concepts/attributes to make models that approximate the system while preserving the fundamentals that we're interested in.
+EXERCISE: If you've studied physics, there's a great example of this in statics and dynamics. Suppose I drop a coin from the top of the science library, and ask you what its velocity will be when it hits the ground. Using the methods you learn in beginning physics, what's something you usefully disregard?
+
+
+Think, then click!
+Air resistance! Friction! We can still get a reasonable approximation for many problems without needing to include that. (And advanced physics adds even more factors that aren't worth considering at this scale.) The model without friction is often enough.
+Systems vs. Models (and Implementations)
+When we say "systems" in this module, we mean the term broadly. A distributed system (like replication in MongoDB) is a system, but so are user interfaces and hardware devices like CPUs and insulin pumps. Git is a system for version control. The web stack, cryptographic protocols, chemical reactions, the rules of sports and games---these are all systems too!
+To help build intuition, let's work with a simple system: the game of tic-tac-toe (also called noughts and crosses). There are many implementations of this game, including this one that Tim wrote for these notes in Python. And, of course, these implementations often have corresponding test suites, like this (incomplete) example.
+Exercise: Play a quick game of tic-tac-toe by hand. If you can, find a partner, but if not, then play by yourself.
+Notice what just happened. You played the game. In doing so, you ran your own mental implementation of the rules. The result you got was one of many possible games, each with its own specific sequence of legal moves, leading to a particular ending state. Maybe someone won, or maybe the game was a tie. Either way, many different games could have ended with that same board.
+Modeling is different from programming. When you're programming traditionally, you give the computer a set of instructions and it follows them. This is true whether you're programming functionally or imperatively, with or without objects, etc. Declarative modeling languages like Forge work differently. The goal of a model isn't to run instructions, but rather to describe the rules that govern systems.
+Here's a useful comparison to help reinforce the difference (with thanks to Daniel Jackson):
+-
+
- An empty program does nothing. +
- An empty model allows every behavior. +
Modeling Tic-Tac-Toe Boards
+What are the essential concepts in a game of tic-tac-toe?
+
+
+
+
+
+When we're first writing a model, we'll start with 5 steps. For each step, I'll give examples from tic-tac-toe and also for binary search trees (which we'll start modeling soon) for contrast.
+-
+
- What are the datatypes involved, and their fields?
+
-
+
- For tic-tac-toe: they might be the 3-by-3 board and the
XandOmarks that go in board locations.
+ - For a binary search tree: they might be the tree nodes and their left and right children. +
+ - For tic-tac-toe: they might be the 3-by-3 board and the
- What makes an instance of these datatypes well formed? That is, what conditions are needed for them to not be garbage?
+
-
+
- For tic-tac-toe, we might require that the indexes used are between
0and2, since the board is 3-by-3.
+ - For a binary search tree, we might require that every node has at most one left child, at most one right child, a unique parent, ... +
+ - For tic-tac-toe, we might require that the indexes used are between
- What's a small example of how these datatypes can be instantiated?
+
-
+
- For tic-tac-toe, the empty board would be an example. So would the board where
Xmoves first into the middle square.
+ - For a binary search tree, this might be a tree with only one node, or a 3-node tree where the root's left and right children are leaves. +
+ - For tic-tac-toe, the empty board would be an example. So would the board where
- What does the model look like when run?
+
-
+
- For tic-tac-toe, we should see a board with some number of
XandOmarks.
+ - For a binary search tree, we should see some set of nodes that forms a single tree via left- and right-children. +
+ - For tic-tac-toe, we should see a board with some number of
- What domain predicates are there? Well-formedness defines conditions that are needed for an instantiation to not be "garbage". But whatever we're modeling surely has domain-specific concepts of its own, which may or may not hold.
+
-
+
- For tic-tac-toe, we care a great deal if the board is a winning board or not. Similarly, we might care if it looks like someone has cheated. +
- For a binary search tree, we care if the tree is balanced, or if it satisfies the BST invariant. +
+
+
+
+
+
+Why make this distinction between well-formedness and domain predicates? Because one should always hold in any instance Forge considers, but the other may or may not hold. In fact, we might want to use Forge to verify that a domain predicate always holds! And if we've told Forge that any instance that doesn't satisfy it is garbage, Forge won't find us such an instance.
+Datatypes
+We might list:
+-
+
- the players
XandO;
+ - the 3-by-3 game board, where players can put their marks; +
- the idea of whose turn it is at any given time; and +
- the idea of who has won the game at any given time. +
Now let's add those ideas to a model in Forge!
+#lang forge/froglet
+The first line of any Forge model will be a #lang line, which says which Forge language the file uses. We'll start with the Froglet language for now. Everything you learn in this language will apply in other Forge languages, so I'll use "Forge" interchangeably.
Now we need a way to talk about the noughts and crosses themselves. So let's add a sig that represents them:
#lang forge/froglet
+abstract sig Player {}
+one sig X, O extends Player {}
+You can think of sig in Forge as declaring a kind of object. A sig can extend another, in which case we say that it is a child of its parent, and child sigs cannot overlap. When a sig is abstract, any member must also be a member of one of that sig's children; in this case, any Player must either be X or O. Finally, a one sig has exactly one member---there's only a single X and O in our model.
We also need a way to represent the game board. We have a few options here: we could create an Index sig, and encode an ordering on those (something like "column A, then column B, then column C"). Another is to use Forge's integer support. Both solutions have their pros and cons. Let's use integers, in part to get some practice with them.
#lang forge/froglet
+abstract sig Player {}
+one sig X, O extends Player {}
+
+sig Board {
+ board: pfunc Int -> Int -> Player
+}
+Every Board object contains a board field describing the moves made so far. This field is a partial function, or dictionary, for every Board that maps each (Int, Int) pair to at most one Player.
Well-formedness
+These definitions sketch the overall shape of a board: players, marks on the board, and so on. But not all boards that fit the definition will be valid. For example:
+-
+
- Forge integers aren't true mathematical integers, but are bounded by a bitwidth we give whenever we run the tool. So we need to be careful here. We want a classical 3-by-3 board with indexes of (say)
0,1, and2, not a board where (e.g.) row-5, column-1is a valid location.
+
We'll call these well-formedness constraints. They aren't innately enforced by our sig declarations, but we'll almost always want Forge to enforce them, so that it doesn't find "garbage instances". Let's write a wellformedness predicate:
-- a Board is well-formed if and only if:
+pred wellformed[b: Board] {
+ -- row and column numbers used are between 0 and 2, inclusive
+ all row, col: Int | {
+ (row < 0 or row > 2 or col < 0 or col > 2)
+ implies no b.board[row][col]
+ }
+}
+This predicate is true of any Board if and only if the above 2 constraints are satisfied. Let's break down the syntax:
-
+
- Constraints can quantify over a domain. E.g.,
all row, col: Int | ...says that for any pair of integers (up to the given bidwidth), the following condition (...) must hold. Forge also supports, e.g., existential quantification (some), but we don't need that yet. We also have access to standard boolean operators likeor,implies, etc.
+ - Formulas in Forge always evaluate to a boolean; expressions evaluate to sets. For example,
+
-
+
- the expression
b.board[row][col]evaluates to thePlayer(if any) with a mark at location (row,col) in boardb; but
+ - the formula
no b.board[row][col]is true if and only if there is no such `Player``.
+
+ - the expression
- A
pred(predicate) in Forge is a helper function that evaluates to a boolean. Thus, its body should always be a formula.
+
+
+
+
+
+Notice that, rather than describing a process that produces a well-formed board, or even instructions to check well-formedness, we've just given a declarative description of what's necessary and sufficient for a board to be well-formed. If we'd left the predicate body empty, any board would be considered well-formed---there'd be no formulas to enforce!
+A Few Examples
+Since a predicate is just a function that returns true or false, depending on its arguments and whichever instance Forge is looking at, we can write tests for it the same way we would for any other boolean-valued function. But even if we're not testing, it can be useful to write a small number of examples, so we can build intuition for what the predicate means.
+We'll write two examples in Forge:
+-- Helper to make these examples easier to write
+pred all_wellformed { all b: Board | wellformed[b]}
+
+-- all_wellformed should be _true_ for the following instance
+example firstRowX_wellformed is {all_wellformed} for {
+ Board = `Board0 -- backquote labels atoms
+ X = `X O = `O -- examples must define all sigs
+ Player = X + O
+ `Board0.board = (0, 0) -> `X + -- examples must define all fields
+ (0, 1) -> `X + -- here, the partial function for
+ (0, 2) -> `X -- the board (empty squares remain empty)
+}
+
+-- all_wellformed should be _false_ for the following instance
+example off_board_not_wellformed is {not all_wellformed} for {
+ Board = `Board0
+ X = `X O = `O
+ Player = X + O
+ `Board0.board = (-1, 0) -> `X +
+ (0, 1) -> `X +
+ (0, 2) -> `X
+}
+In Forge, examples are automatically run whenever your model executes. They describe basic intent about a given predicate; in this case, we're testing that a board where X has moved 3 times in valid locations is considered well formed. In contrast, if X has moved in an invalid location, it won't be considered well formed. Again, we're not making judgements about the rules being obeyed yet—just about whether our model is conforming to how we've encoded the game, using 0, 1, and 2 as the only valid indexes.
+
+
+
+
+Notice that we've got a test thats a positive example and another test that's a negative example. We want to make sure to exercise both cases, or else "always true" or "always" false could pass our suite.
+Running Forge
+The run command tells Forge to search for an instance satisfying the given constraints:
run { some b: Board | wellformed[b]}
+When we click the play button in the VSCode extension, the engine solves the constraints and produces a satisfying instance, (Because of differences across solver versions, hardware, etc., it's possible you'll see a different instance than the one shown here.) A browser window should pop up with a visualization. You can also run racket <filename.frg> in the terminal, although we recommend the VSCode extension.
+
+
+
+
+If you're running on Windows, the Windows-native cmd and PowerShell terminals will not properly load Forge's visualizer. Instead, we suggest using one of many other options on Windows that we've tested and know to work: the VSCode extension (available on the VSCode Marketplace), DrRacket, Git bash, Windows Subsystem for Linux, or Cygwin.
+
There are many options for visualization. The default which loads initially is a directed-graph based one:
+This isn't very useful; it looks nothing like a tic-tac-toe board! We can make more progress by using the "Table" visualization---which isn't ideal either:
+Forge also allows users to make custom visualizations via short JavaScript programs; here's an example basic visualizer for this specific tic-tac-toe model that produces images like this one:
+We'll talk more about visualization scripts later. For now, let's proceed. TODO: replace img with one matching the table view +TODO: add side-by-side CSS
++
This instance contains a single board, and it has 9 entries. Player O has moved in all of them (the 0 suffix of O0 in the display is an artifact of how Forge's engine works; ignore it for now). It's worth noticing two things:
-
+
- This board doesn't look quite right: player
Ooccupies all the squares. We might ask: has playerObeen cheating? But the fact is that this board satisfies the constraints we have written so far. Forge produces it simply because our model isn't yet restrictive enough, and for no other reason. "Cheating" doesn't exist yet.
+ - We didn't say how to find that instance. We just said what we wanted, and the tool performed some kind of search to find it. So far the objects are simple, and the constraints basic, but hopefully the power of the idea is coming into focus. +
Reflection: Implementation vs. Model
+So far we've just modeled boards, not full games. But we can still contrast our work here against the implementation of tic-tac-toe shared above. We might ask:
+-
+
- How do the data-structure choices, and type declarations, in the implementation compare with the model? +
- Is there an implementation that matches what we just did? (The program's purpose isn't to generate boards, but to play games!) +
Domain Predicates
+Now let's write predicates that describe important ideas in the domain. What's important in the game of tic-tac-toe? Here are a few things.
+Starting Boards
+What would it mean to be a starting state in a game? The board is empty:
+pred starting[s: Board] {
+ all row, col: Int |
+ no s.board[row][col]
+}
+Turns
+How do we tell when it's a given player's turn? It's X's turn when there are the same number of each mark on the board:
pred XTurn[s: Board] {
+ #{row, col: Int | s.board[row][col] = X} =
+ #{row, col: Int | s.board[row][col] = O}
+}
+The {row, col: Int | ...} syntax means a set comprehension, and describes the set of row-column pairs where the board contains X (or O). The # operator gives the size of these sets, which we then compare.
Question: Is it enough to say that OTurn is the negation of XTurn?
+
+Think, then click!
+No! At least not in the model as currently written. If you're curious to see why, run the model and look at the instances produced. Instead, we need to say something like this:
+pred OTurn[s: Board] {
+ #{row, col: Int | s.board[row][col] = X} =
+ add[#{row, col: Int | s.board[row][col] = O}, 1]
+}
+
+
+
+
+
+Forge supports arithmetic operations on integers like add. While it doesn't matter for this model yet, addition (and other operations) can overflow according to 2's complement arithmetic. For example, if we're working with 4-bit integers, then add[7,1] will be -8. You can experiment with this in the visualizer's evaluator, which we'll be using a lot after the initial modeling tour is done.
+
+
+
+
+Don't try to use + for addition in any Forge language. Use add instead; this is because + is reserved for something else (which we'll explain later).
Winning the Game
+What does it mean to win? A player has won on a given board if:
+-
+
- they have placed their mark in all 3 columns of a row; +
- they have placed their mark in all 3 rows of a column; or +
- they have placed their mark in all 3 squares of a diagonal. +
We'll express this in a winner predicate that takes the current board and a player name. Let's also define a couple helper predicates along the way:
pred winRow[s: Board, p: Player] {
+ -- note we cannot use `all` here because there are more Ints
+ some row: Int | {
+ s.board[row][0] = p
+ s.board[row][1] = p
+ s.board[row][2] = p
+ }
+}
+
+pred winCol[s: Board, p: Player] {
+ some column: Int | {
+ s.board[0][column] = p
+ s.board[1][column] = p
+ s.board[2][column] = p
+ }
+}
+
+pred winner[s: Board, p: Player] {
+ winRow[s, p]
+ or
+ winCol[s, p]
+ or
+ {
+ s.board[0][0] = p
+ s.board[1][1] = p
+ s.board[2][2] = p
+ } or {
+ s.board[0][2] = p
+ s.board[1][1] = p
+ s.board[2][0] = p
+ }
+}
+After writing these domain predicates, we're reaching a fairly complete model for a single tic-tac-toe board. Let's decide how to fix the issue we saw above (the reason why OTurn couldn't be the negation of XTurn): perhaps a player has moved too often.
Should we add something like OTurn[s] or XTurn[s] to our wellformedness predicate? No! If we then later enforced wellformedness for all boards, that would exclude "cheating" instances where a player has more moves on the board than are allowed. But this has some risk, depending on how we intend to use the wellformed predicate:
-
+
- If we were only ever generating valid boards, a cheating state might well be spurious, or at least undesirable. In that case, we might prevent such states in
wellformedand rule it out.
+ - If we were generating arbitrary (not necessarily valid) boards, being able to see a cheating state might be useful. In that case, we'd leave it out of
wellformed.
+ - If we're interested in verification, e.g., we are asking whether the game of Tic-Tac-Toe enables ever reaching a cheating board, we shouldn't add
not cheatingtowellformed; becausewellformedalso excludes garbage boards, we'd probably use it in our verification—in which case, Forge will never find us a counterexample!
+
[TODO: move this point to position it properly, if PBT comes after vs. before]
+
+
+
+
+
+Notice the similarity between this issue and what we do in property-based testing. Here, we're forced to distinguish between what a reasonable board is (analogous to the generator's output in PBT) and what a reasonable behavior is (analogous to the validity predicate in PBT). One narrows the scope of possible worlds to avoid true "garbage"; the other checks whether the system behaves as expected in one of those worlds.
+We'll come back to this later, when we've had a bit more modeling experience. For now, let's separate our goal into a new predicate called balanced, and add it to our run command above:
pred balanced[s: Board] {
+ XTurn[s] or OTurn[s]
+}
+run { some b: Board | wellformed[b] and balanced[b]}
+If we click the "Next" button a few times, we see that not all is well: we're getting boards where wellformed is violated (e.g., entries at negative rows, or multiple moves in one square).
We're getting this because of how the run was phrased. We said to find an instance where some board was well-formed and valid, not one where all boards were. By default, Forge will find instances with up to 4 Boards. So we can fix the problem either by telling Forge to find instances with only 1 Board:
run { some b: Board | wellformed[b] and balanced[b]}
+for exactly 1 Board
+or by saying that all boards must be well-formed and balanced:
+run { all b: Board | wellformed[b] and balanced[b]}
+Practice with run
+The run command can be used to give Forge more detailed instructions for its search.
No Boards
+Is it possible for an instance with no boards to still satisfy constraints like these?
+run {
+ all b: Board | {
+ -- X has won, and the board looks OK
+ wellformed[b]
+ winner[b, X]
+ balanced[b]
+ }
+ }
+
+
+Think, then click!
+Yes! There aren't any boards, so there's no obligation for anything to satisfy the constraints inside the quantifier. You can think of the all as something like a for loop in Java or the all() function in Python: it checks every Board in the instance. If there aren't any, there's nothing to check—return true.
Adding More
+This addition also requires that X moved in the middle of the board:
run {
+ all b: Board | {
+ -- X has won, and the board looks OK
+ wellformed[b]
+ winner[b, X]
+ balanced[b]
+ -- X started in the middle
+ b.board[1][1] = X
+ }
+ } for exactly 2 Board
+Notice that, because we said exactly 2 Board here, Forge must find instances containing 2 tic-tac-toe boards, and both of them must satisfy the constraints: wellformedness, X moving in the middle, etc. You could ask for a board where X hasn't won by adding not winner[b, X].
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/clipboard.min.js b/clipboard.min.js
new file mode 100644
index 0000000..02c549e
--- /dev/null
+++ b/clipboard.min.js
@@ -0,0 +1,7 @@
+/*!
+ * clipboard.js v2.0.4
+ * https://zenorocha.github.io/clipboard.js
+ *
+ * Licensed MIT © Zeno Rocha
+ */
+!function(t,e){"object"==typeof exports&&"object"==typeof module?module.exports=e():"function"==typeof define&&define.amd?define([],e):"object"==typeof exports?exports.ClipboardJS=e():t.ClipboardJS=e()}(this,function(){return function(n){var o={};function r(t){if(o[t])return o[t].exports;var e=o[t]={i:t,l:!1,exports:{}};return n[t].call(e.exports,e,e.exports,r),e.l=!0,e.exports}return r.m=n,r.c=o,r.d=function(t,e,n){r.o(t,e)||Object.defineProperty(t,e,{enumerable:!0,get:n})},r.r=function(t){"undefined"!=typeof Symbol&&Symbol.toStringTag&&Object.defineProperty(t,Symbol.toStringTag,{value:"Module"}),Object.defineProperty(t,"__esModule",{value:!0})},r.t=function(e,t){if(1&t&&(e=r(e)),8&t)return e;if(4&t&&"object"==typeof e&&e&&e.__esModule)return e;var n=Object.create(null);if(r.r(n),Object.defineProperty(n,"default",{enumerable:!0,value:e}),2&t&&"string"!=typeof e)for(var o in e)r.d(n,o,function(t){return e[t]}.bind(null,o));return n},r.n=function(t){var e=t&&t.__esModule?function(){return t.default}:function(){return t};return r.d(e,"a",e),e},r.o=function(t,e){return Object.prototype.hasOwnProperty.call(t,e)},r.p="",r(r.s=0)}([function(t,e,n){"use strict";var r="function"==typeof Symbol&&"symbol"==typeof Symbol.iterator?function(t){return typeof t}:function(t){return t&&"function"==typeof Symbol&&t.constructor===Symbol&&t!==Symbol.prototype?"symbol":typeof t},i=function(){function o(t,e){for(var n=0;n
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+There Exists
+
+
+
+
+ From Boards to Games
+What do you think a game of tic-tac-toe looks like? How should we model the moves between board states?
+
+
+Think, then click!
+It's often convenient to think of the game as a big graph, where the nodes are the states (possible board configurations) and the edges are transitions (in this case, legal moves of the game). Here's a rough sketch:
+
+
A game of tic-tac-toe is a sequence of steps in this graph, starting from the empty board. Let's model it.
+First, what does a move look like? A player puts their mark at a specific location. In Alloy, we'll represent this using a transition predicate: a predicate that says when it's legal for one state to evolve into another. We'll often call these the pre-state and post-state of the transition:
+pred move[pre: Board, row: Int, col: Int, p: Player, post: Board] {
+ // ...
+}
+What constraints should we add? It's useful to divide the contents of such a predicate into:
+-
+
- a guard, which allows the move only if the pre-state is suitable; and +
- an action, which defines what is in the post-state based on the pre-state and the move parameters. +
For the guard, in order for the move to be valid, it must hold that in the pre-state:
+-
+
- nobody has already moved at the target location; and +
- it's the moving player's turn. +
For the action:
+-
+
- the new board is the same as the old, except for the addition of the player's mark at the target location. +
Now we can fill in the predicate. Let's try something like this:
+pred move[pre: Board, row: Int, col: Int, p: Player, post: Board] {
+ -- guard:
+ no pre.board[row][col] -- nobody's moved there yet
+ p = X implies XTurn[pre] -- appropriate turn
+ p = O implies OTurn[pre]
+
+ -- action:
+ post.board[row][col] = p
+ all row2: Int, col2: Int | (row!=row2 and col!=col2) implies {
+ post.board[row2][col2] = pre.board[row2][col2]
+ }
+}
+There are many ways to write this predicate. However, we're going to stick with this form because it calls out an important point. Suppose we had only written post.board[row][col] = p for the action, without the all on the next following lines. Those added lines, which we'll call a frame condition, say that all other squares remain unchanged; without them, the contents of any other square might change in any way. Leaving them out would cause an underconstraint bug: the predicate would be too weak to accurately describe moves in tic-tac-toe.
Exercise: comment out the 3 frame-condition lines and run the model. Do you see moves where the other 8 squares change arbitrarily?
+Exercise: could there be a bug in this predicate? (Run Forge and find out!)
+
+
+
+
+Think, then click
+The all row2... formula says that for any board location where both the row and column differ from the move's, the board remains the same. But is that what we really wanted? Suppose X moves at location 1, 1. Then of the 9 locations, which is actually protected?
| Row | Column | Protected? |
|---|---|---|
| 0 | 0 | yes |
| 0 | 1 | no (column 1 = column 1) |
| 0 | 2 | yes |
| 1 | 0 | no (row 1 = row 1) |
| 1 | 1 | no (as intended) |
| 1 | 2 | no (row 1 = row 1) |
| 2 | 0 | yes |
| 2 | 1 | no (column 1 = column 1) |
| 2 | 2 | yes |
Our frame condition was too weak! We need to have it take effect whenever either the row or column is different. Something like this will work:
+ all row2: Int, col2: Int |
+ ((row2 != row) or (col2 != col)) implies {
+ post.board[row2][col2] = pre.board[row2][col2]
+ }
+
+A Simple Property
+Once someone wins a game, does their win still persist, even if more moves are made? I'd like to think so: moves never get undone, and in our model winning just means the existence of 3-in-a-row for some player. We probably even believe this property without checking it. However, it won't always be so straightforward to show that properties are preserved by the system. We'll check this one in Forge as an example of how you might prove something similar in a more complex system.
+
+
+
+
+
+This is our first step into the world of verification. Asking whether or not a program, algorithm, or other system always satisfies some assertion is a core problem in formal methods, and has a long and storied history.
+We'll tell Forge to find us pairs of states, connected by a move: the pre-state before the move, and the post-state after it. That's any potential transition in tic-tac-toe. The trick is in adding two more constraints. We'll say that someone has won in the pre-state, but they haven't won in the post-state.
+pred winningPreservedCounterexample {
+ some pre, post: Board | {
+ some row, col: Int, p: Player |
+ move[pre, post, row, col, p]
+ winner[pre, X]
+ not winner[post, X]
+ }
+}
+run {
+ all s: Board | wellformed[s]
+ winningPreservedCounterexample
+}
+The check passes---Forge can't find any counterexamples. We'll see this reported as "UNSAT" in the visualizer.
+ +Generating Complete Games
+Recall that our worldview for this model is that systems transition between states, and thus we can think of a system as a directed graph. If the transitions have arguments, we'll sometimes label the edges of the graph with those arguments. This view is sometimes called a discrete event model, because one event happens at a time. Here, the events are moves of the game. In a bigger model, there might be many different types of events.
+TODO: I think this goes later in the book, we don't want to start on finite traces yet.
+Today, we'll ask Forge to find us traces of the system, starting from an initial state. We'll also add a Game sig to incorporate some metadata.
one sig Game {
+ initialState: one Board,
+ next: pfunc Board -> Board
+}
+
+pred traces {
+ -- The trace starts with an initial state
+ starting[Game.initialState]
+ no sprev: Board | Game.next[sprev] = Game.initialState
+ -- Every transition is a valid move
+ all s: Board | some Game.next[s] implies {
+ some row, col: Int, p: Player |
+ move[s, row, col, p, Game.next[s]]
+ }
+}
+By itself, this wouldn't be quite enough; we might see a bunch of disjoint traces. We could add more constraints manually, but there's a better option: tell Forge, at runtime, that next represents a linear ordering on states.
run {
+ traces
+} for {next is linear}
+The key thing to notice here is that next is linear isn't a constraint; it's a separate annotation given to Forge alongside a run or a test. Never put such an annotation in a constraint block; Forge won't understand it. These annotations narrow Forge's bounds (the space of possible worlds to check) which means they can often make problems more efficient for Forge to solve.
In general, Forge accepts such annotations after numeric bounds. E.g., if we wanted to see full games, rather than unfinished game prefixes (the default bound on any sig, including Board, is up to 4) we could have asked:
run {
+ traces
+} for exactly 10 Board for {next is linear}
+You might notice that because of this, some traces are excluded. That's because next is linear forces exact bounds on Board. More on this next time.
The Evaluator
+Moreover, since we're now viewing a single fixed instance, we can evaluate Forge expressions in it. This is great for debugging, but also for just understanding Forge a little bit better. Open the evaluator here at the bottom of the right-side tray, under theming. Then enter an expression or constraint here:
+
Type in something like some s: State | winner[s, X]. Forge should give you either #t (for true) or #f (for false) depending on whether the game shows X winning the game.
Optimizing
+You might notice that this model takes a while to run, after we start reasoning about full games. Why might that be? Let's re-examine our bounds and see if there's anything we can adjust. In particular, here's what the evaluator says we've got for integers:
+
Wow---wait, do we really need to be able to count up to 7 for this model? Probably not. If we change our integer bounds to 3 Int we'll still be able to use 0, 1, and 2, and the search space is much smaller.
Anticipated Questions
+TODO: much of this should be moved later
+A Visual Sketch of How Forge Searches
+Suppose we're using Forge to search for family trees. There are infinitely many potential family tree instances, but Forge needs to work with a finite search space. This is where the bounds of a run come in; they limit the set of instances Forge will even consider. Constraints you write are not yet involved at this point.
Once the bounded search space has been established, Forge uses the constraints you write to find satisfying instances within the bounded search space.
+
The engine uses bounds and constraints very differently, and inferring constraints is often less efficient than inferring bounds. But the engine treats them differently, which means sometimes the distinction leaks through.
+"Nulls" in Forge
+In Forge, there is a special value called none. It's analogous (but not the same!) to a null in languages like Java.
Suppose I added this predicate to our run command in the tic-tac-toe model:
pred myIdea {
+ all row1, col1, row2, col2: Int |
+ (row1 != row2 or col1 != col2) implies
+ Game.initialState.board[row1][col1] !=
+ Game.initialState.board[row2][col2]
+}
+I'm trying to express that every entry in the board is different. This should easily be true about the initial board, as there are no pieces there.
+For context, recall that we had defined a Game sig earlier:
one sig Game {
+ initialState: one State,
+ nextState: pfunc State -> State
+}
+What do you think would happen?
+
+
+Think (or try it in Forge) then click!
+It's very likely this predicate would be unsatisfiable, given the constraints on the initial state. Why?
+Because none equals itself! We can check this:
test expect {
+ nullity: {none != none} is unsat
+}
+Thus, when you're writing constraints like the above, you need to watch out for none: the value for every cell in the initial board is equal to the value for every other cell!
+
+
+
+
+The none value in Forge has at least one more subtlety: none is "reachable" from everything if you're using the built-in reachable helper predicate. That has an impact even if we don't use none explicitly. If I write something like: reachable[p.spouse, Nim, parent1, parent2] I'm asking whether, for some person p, their spouse is an ancestor of Nim. If p doesn't have a spouse, then p.spouse is none, and so this predicate would yield true for p.
Some as a Quantifier Versus Some as a Multiplicity
+The keyword some is used in 2 different ways in Forge:
-
+
- it's a quantifier, as in
some b: Board, p: Player | winner[s, p], which says that somebody has won in some board; and
+ - it's a multiplicity operator, as in
some Game.initialState.board[1][1], which says that that cell of the initial board is populated.
+
Implies vs. Such That
+You can read some row : Int | ... as "There exists some integer row such that ...". The transliteration isn't quite as nice for all; it's better to read all row : Int | ... as "In all integer rows, it holds that ...".
If you want to further restrict the values used in an all, you'd use implies. But if you want to add additional requirements for a some, you'd use and. Here are 2 examples:
-
+
- All: "Everybody who has a
parent1doesn't also have that person as theirparent2":all p: Person | some p.parent1 implies p.parent1 != p.parent2.
+ - Some: "There exists someone who has a
parent1and aspouse":some p: Person | some p.parent1 and some p.spouse.
+
Technical aside: The type designation on the variable can be interpreted as having a character similar to these add-ons: and (for some) and implies (for all). E.g., "there exists some row such that row is an integer and ...", or "In all rows, if row is an integer, it holds that...".
There Exists some Atom vs. Some Instance
+Forge searches for instances that satisfy the constraints you give it. Every run in Forge is about satisfiability; answering the question "Does there exist an instance, such that...".
Crucially, you cannot write a Forge constraint that quantifies over instances themselves. You can ask Forge "does there exist an instance such that...", which is pretty flexible on its own. E.g., if you want to check that something holds of all instances, you can ask Forge to find counterexamples. This is how assert ... is necessary for ... is implemented, and how the examples from last week worked.
One Versus Some
+The one quantifier is for saying "there exists a UNIQUE ...". As a result, there are hidden constraints embedded into its use. one x: A | myPred[x] really means, roughly, some x: A | myPred[x] and all x2: A | not myPred[x]. This means that interleaving one with other quantifiers can be subtle; for that reason, we won't use it except for very simple constraints.
If you use quantifiers other than some and all, beware. They're convenient, but various issues can arise.
Testing Predicate Equivalence
+Checking whether or not two predicates are equivalent is the core of quite a few Forge applications---and a great debugging technique sometimes.
+How do you do it? Like this:
+pred myPred1 {
+ some i1, i2: Int | i1 = i2
+}
+pred myPred2 {
+ not all i2, i1: Int | i1 != i2
+}
+assert myPred1 is necessary for myPred2
+assert myPred2 is necessary for myPred1
+If you get an instance where the two predicates aren't equivalent, you can use the Sterling evaluator to find out why. Try different subexpressions, discover which is producing an unexpected result! E.g., if we had written (forgetting the not):
pred myPred2 {
+ all i2, i1: Int | i1 != i2
+}
+One of the assertions would fail, yielding an instance in Sterling you could use the evaluator with.
+More Testing Syntax and a Lesson
+I'm not going to use this syntax in class if I don't need to, because it's less intentional. But using it here lets me highlight a common conceptual issue with Forge in general.
+test expect {
+ -- correct: "no counterexample exists"
+ p1eqp2_A: {
+ not (myPred1 iff myPred2)
+ } is unsat
+ -- incorrect: "it's possible to satisfy what i think always holds"
+ p1eqp2_B: {
+ myPred1 iff myPred2
+ } is sat
+
+}
+These two tests do not express the same thing! One asks Forge to find an instance where the predicates are not equivalent (this is what we want). The other asks Forge to find an instance where they are equivalent (this is what we're hoping holds for any instance, not just one)!
+ +":e:f.tabReplace?e.replace(/\t/g,f.tabReplace):e):e}function E(e){let n=null;const t=function(e){var n=e.className+" ";n+=e.parentNode?e.parentNode.className:"";const t=f.languageDetectRe.exec(n);if(t){var r=T(t[1]);return r||(console.warn(g.replace("{}",t[1])),console.warn("Falling back to no-highlight mode for this block.",e)),r?t[1]:"no-highlight"}return n.split(/\s+/).find(e=>p(e)||T(e))}(e);if(p(t))return;S("before:highlightBlock",{block:e,language:t}),f.useBR?(n=document.createElement("div")).innerHTML=e.innerHTML.replace(/\n/g,"").replace(/
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/mark.min.js b/mark.min.js
new file mode 100644
index 0000000..1636231
--- /dev/null
+++ b/mark.min.js
@@ -0,0 +1,7 @@
+/*!***************************************************
+* mark.js v8.11.1
+* https://markjs.io/
+* Copyright (c) 2014–2018, Julian Kühnel
+* Released under the MIT license https://git.io/vwTVl
+*****************************************************/
+!function(e,t){"object"==typeof exports&&"undefined"!=typeof module?module.exports=t():"function"==typeof define&&define.amd?define(t):e.Mark=t()}(this,function(){"use strict";var e="function"==typeof Symbol&&"symbol"==typeof Symbol.iterator?function(e){return typeof e}:function(e){return e&&"function"==typeof Symbol&&e.constructor===Symbol&&e!==Symbol.prototype?"symbol":typeof e},t=function(e,t){if(!(e instanceof t))throw new TypeError("Cannot call a class as a function")},n=function(){function e(e,t){for(var n=0;n
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Logic for Systems
+Setting the Stage
+If you're taking this course or reading this book, you've probably had to complete some programming assignments---or at least written some small program for a course or an online tutorial. Take a moment to list a handful of such assignments: what did you have to build?
+Now ask yourself:
+-
+
- How did you know what behavior to implement? +
- How did you know which data structures or algorithms were the right ones to use? +
- How did you know your program "worked", in the end? +
In the context of a course, there are "expected" answers to these questions. For instance, you might say you know your code worked because you tested it (very thoroughly)! But is that really the truth? In terms of consequences, the true bar for excellent in a programming class is the grade you got. That is:
+-
+
- You knew what to do because you were told what to do. +
- You probably knew which algorithms to use because they'd just been taught to you. +
- You were confident that your programs worked because you were told by an authority figure. +
But outside that context, as (say) a professional engineer, you lose the safety net. You might be working on a program that controls the fate of billions of dollars, tempers geopolitical strife, or controls a patient's insulin pump. Even if you had a TA, would you trust them to tell you that those programs worked? Would you trust your boss to understand exactly what needed to happen, and tell you exactly how to do it? Probably not! Instead, you need to think carefully about what you want, how to build it, and how to evaluate what you and others have built.
+
+
+
+
+
+As engineers, we strive for perfection. But perfection is an ideal; it's not obtainable. Why? First: we're human. Even if we could read our customers' minds, that's no guarantee that they know what they really need. And even if we can prove our code is correct, we might be checking for the wrong things. Second: our environment is hostile. Computers break. Patches to dependencies introduce errors. Cosmic radiation can flip bits in memory. 100% reliability is hopeless. Anyone who tells you differently is trying to sell you something.
+But that doesn't mean we should give up. It just means that we should moderate our expectations. This book won't teach you how to never make mistakes. Instead, it will teach you a multiple ways to increase your confidence in correctness.
+Unit Testing
+Let's start with unit-testing and deconstruct it. What does it do well? What does it do poorly?
+Exercise: Make two lists to answer the above question. Why do we test? What could go wrong, and how can the sort of testing you've done in other classes let us down?
+Hopefully we all agree that concrete input-output testing has its virtues and that we should keep doing it. But let's focus on the things that testing doesn't do well.
+
+
+Think, then click!
+You might have observed that (for most interesting programs, anyway) tests cannot be exhaustive because there are infinitely many possible inputs. And since we're forced to test non-exhaustively, we have to hope we pick good tests---tests that not only focus on our own implementation, but on others (like the implementation that replaces yours eventually) too.
+Worse, we can't test the things we don't think of, or don't know about; we're vulnerable to our limited knowledge, the availability heuristic, confirmation bias, and so on. In fact, we humans are generally ill equipped for logical reasoning, even if trained.
+Humans and Reasoning
+A Toy Example
+Suppose we're thinking about the workings of a small company. We're given some facts about the company, and have to answer a question based on those facts. Here's an example. We know that:
+-
+
- Alice supervises Bob. +
- Bob supervises Charlie. +
- Alice graduated Brown. +
- Charlie graduated Harvale. +
Question: Does someone who graduated from Brown directly supervise someone who graduated from another University?
+
+
+Think, then click.
+Yes! Regardless of whether Bob graduated from Brown, some Brown graduate supervises some non-Brown graduate. Reasoning by hypotheticals, there is one fact we don't know: where Bob graduated. In case he graduated Brown, he supervises Charlie, a non-Brown graduate. In case he graduated from another school, he's supervised by Alice, a Brown graduate.
+Humans tend to be very bad at reasoning by hypotheticals. There's a temptation to think that this puzzle isn't solvable because we don't know where Bob graduated from. Even Tim thought this at first after seeing the puzzle—in grad school! For logic!
+Now imagine a puzzle with a thousand of these unknowns. A thousand boolean variables means cases to reason through. Want to use a computer yet?
+ +Of course, this isn't really about logic puzzles.
+A Real Scenario
+There's a real cryptographic protocol called the Needham-Schroeder public-key protocol. You can read about it here. Unfortunately the protocol has a bug: it's vulnerable to attack if one of the principles can be fooled into starting an exchange with a badly-behaved or compromised agent. We won't go into specifics. Instead, let's focus on the fact that it's quite easy to get things like protocols wrong, and sometimes challenging for us humans to completely explore all possible behaviors -- especially since there might be behaviors we'd never even considered! It sure would be nice if we could get a computer to help out with that.
+A pair of former 1710 students did an ISP on modeling crypto protocols, using the tools you'll learn in class. Here's an example picture, generated by their model, of the flaw in the Needham-Schroeder protocol:
+
You don't need to understand the specifics of the visualization; the point is that someone who has studied crypto protocols would. And this really does show the classic attack on Needham-Schroeder. You may not be a crypto-protocol person, but you probably are an expert in something you'd like to model, and you might very well get the chance to do so this semester.
+Automated Reasoning as an Assistive Device
+The human species has been so successful, in part, because of our ability to use assistive devices—tools! Eyeglasses, bicycles, hammers, bridges: all devices that assist us in navigating the world in our fragile meat-bodies. One of our oldest inventions, writing, is an assistive device that increases our long-term memory space and makes that memory persistent. Computers are only one in a long line of such inventions.
+So, naturally, we've found ways to:
+-
+
- use computers to help us test our ideas; +
- use computers to exhaustively check program correctness; +
- use computers to help us find gaps in our intuition about a program; +
- use computers to help us explore the design space of a data structure, or algorithm, card game, or chemical reaction; +
- etc. +
There's a large body of work in Computer Science that uses logic to do all those things. We tend to call it formal methods, especially when the focus is on reasoning about systems. It touches on topics like system modeling, constraint solving, program analysis, design exploration, and more. That's what this book is about: the foundational knowledge to engage with many different applications of these ideas, even if you don't end up working with them directly every day.
+More concretely, we'll focus on a class of techniques called lightweight formal methods, which are characterized by tradeoffs that favor ease of use over strong guarantees (although we'll sometimes achieve those as well).
+
+
+
+
+
+Jeanette Wing and Daniel Jackson wrote a short article coining the term "lightweight FM" in the 90's, which you can find online.
+
+
+
+
+
+When we say "systems" in this book we don't necessarily mean the kind of systems you see in a class on networks, hardware architecture, or operating systems. You can apply the techniques in this book to those subjects quite naturally, but you can also apply it to user interfaces, type systems in programming, hardware, version control systems like Git, web security, cryptographic protocols, robotics, puzzles, sports and games, and much more. So we construe the word "system" very broadly.
+Here are some examples of "systems" that students have modeled in Forge: lifetimes in Rust, network reachability, and poker!
+The Future of Computing
+For better or worse, The shape of engineering is changing. Lots of people are excited, scared, or both about large language models like ChatGPT. This book won't teach you how to use generative AI, so it's reasonable to wonder: why learn from this book, instead of another AI book?
+There are two questions that will never go out of style, and won't be answered by AI (at least, not in our lifetimes):
+-
+
- What do you want to build? What does your customer really need? Answering this requires talking to them and other stakeholders, watching their processes, seeking their feedback, and adjusting your design based on it. And no matter who (or what) is writing the actual code, you need to be able to express all this precisely enough that they (or it) can succeed at the implementation. +
- How will you evaluate what you get? No matter who (or what) is building the system, verification is needed before the system can be trusted. +
Even setting aside the customer-facing aspects, we'll still need to think critically about what it is we want and how to evaluate whether we're getting it. The skills you learn here will remain useful (or become even more so) as engineering evolves. And those skills will be useful for more than just code.
+ + +Looking Ahead: Tools
+The main tool we'll use in this course is Forge. Forge is a tool for modeling systems; we'll talk about what that means later on. For now, be aware that we'll be progressing through three language levels in Forge:
+-
+
- Froglet, which restricts the set of operations available so that we can jump right in more easily. If you have intuitions about object-oriented programming, those intuitions will be useful in Froglet, although there are a few important differences that we'll talk about. +
- Relational Forge, which expands the set of operations available to include sets, relations, and relational operators. Again, we'll cover these in detail later. They are useful for reasoning about complex relationships between objects and for representing certain domains, like databases or graphs. +
- Temporal Forge, which lets us cleanly model how a system's state evolves over time. +
We'll also use:
+-
+
- Hypothesis, a testing library for Python; and +
- Z3, an SMT solver library. +
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/searcher.js b/searcher.js
new file mode 100644
index 0000000..d2b0aee
--- /dev/null
+++ b/searcher.js
@@ -0,0 +1,483 @@
+"use strict";
+window.search = window.search || {};
+(function search(search) {
+ // Search functionality
+ //
+ // You can use !hasFocus() to prevent keyhandling in your key
+ // event handlers while the user is typing their search.
+
+ if (!Mark || !elasticlunr) {
+ return;
+ }
+
+ //IE 11 Compatibility from https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/String/startsWith
+ if (!String.prototype.startsWith) {
+ String.prototype.startsWith = function(search, pos) {
+ return this.substr(!pos || pos < 0 ? 0 : +pos, search.length) === search;
+ };
+ }
+
+ var search_wrap = document.getElementById('search-wrapper'),
+ searchbar = document.getElementById('searchbar'),
+ searchbar_outer = document.getElementById('searchbar-outer'),
+ searchresults = document.getElementById('searchresults'),
+ searchresults_outer = document.getElementById('searchresults-outer'),
+ searchresults_header = document.getElementById('searchresults-header'),
+ searchicon = document.getElementById('search-toggle'),
+ content = document.getElementById('content'),
+
+ searchindex = null,
+ doc_urls = [],
+ results_options = {
+ teaser_word_count: 30,
+ limit_results: 30,
+ },
+ search_options = {
+ bool: "AND",
+ expand: true,
+ fields: {
+ title: {boost: 1},
+ body: {boost: 1},
+ breadcrumbs: {boost: 0}
+ }
+ },
+ mark_exclude = [],
+ marker = new Mark(content),
+ current_searchterm = "",
+ URL_SEARCH_PARAM = 'search',
+ URL_MARK_PARAM = 'highlight',
+ teaser_count = 0,
+
+ SEARCH_HOTKEY_KEYCODE = 83,
+ ESCAPE_KEYCODE = 27,
+ DOWN_KEYCODE = 40,
+ UP_KEYCODE = 38,
+ SELECT_KEYCODE = 13;
+
+ function hasFocus() {
+ return searchbar === document.activeElement;
+ }
+
+ function removeChildren(elem) {
+ while (elem.firstChild) {
+ elem.removeChild(elem.firstChild);
+ }
+ }
+
+ // Helper to parse a url into its building blocks.
+ function parseURL(url) {
+ var a = document.createElement('a');
+ a.href = url;
+ return {
+ source: url,
+ protocol: a.protocol.replace(':',''),
+ host: a.hostname,
+ port: a.port,
+ params: (function(){
+ var ret = {};
+ var seg = a.search.replace(/^\?/,'').split('&');
+ var len = seg.length, i = 0, s;
+ for (;i
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Practice with
+
+There Exists
+
+
+
+
+ Logic for Systems
+Setting the Stage
+If you're taking this course or reading this book, you've probably had to complete some programming assignments---or at least written some small program for a course or an online tutorial. Take a moment to list a handful of such assignments: what did you have to build?
+Now ask yourself:
+-
+
- How did you know what behavior to implement? +
- How did you know which data structures or algorithms were the right ones to use? +
- How did you know your program "worked", in the end? +
In the context of a course, there are "expected" answers to these questions. For instance, you might say you know your code worked because you tested it (very thoroughly)! But is that really the truth? In terms of consequences, the true bar for excellent in a programming class is the grade you got. That is:
+-
+
- You knew what to do because you were told what to do. +
- You probably knew which algorithms to use because they'd just been taught to you. +
- You were confident that your programs worked because you were told by an authority figure. +
But outside that context, as (say) a professional engineer, you lose the safety net. You might be working on a program that controls the fate of billions of dollars, tempers geopolitical strife, or controls a patient's insulin pump. Even if you had a TA, would you trust them to tell you that those programs worked? Would you trust your boss to understand exactly what needed to happen, and tell you exactly how to do it? Probably not! Instead, you need to think carefully about what you want, how to build it, and how to evaluate what you and others have built.
+
+
+
+
+
+As engineers, we strive for perfection. But perfection is an ideal; it's not obtainable. Why? First: we're human. Even if we could read our customers' minds, that's no guarantee that they know what they really need. And even if we can prove our code is correct, we might be checking for the wrong things. Second: our environment is hostile. Computers break. Patches to dependencies introduce errors. Cosmic radiation can flip bits in memory. 100% reliability is hopeless. Anyone who tells you differently is trying to sell you something.
+But that doesn't mean we should give up. It just means that we should moderate our expectations. This book won't teach you how to never make mistakes. Instead, it will teach you a multiple ways to increase your confidence in correctness.
+Unit Testing
+Let's start with unit-testing and deconstruct it. What does it do well? What does it do poorly?
+Exercise: Make two lists to answer the above question. Why do we test? What could go wrong, and how can the sort of testing you've done in other classes let us down?
+Hopefully we all agree that concrete input-output testing has its virtues and that we should keep doing it. But let's focus on the things that testing doesn't do well.
+
+
+Think, then click!
+You might have observed that (for most interesting programs, anyway) tests cannot be exhaustive because there are infinitely many possible inputs. And since we're forced to test non-exhaustively, we have to hope we pick good tests---tests that not only focus on our own implementation, but on others (like the implementation that replaces yours eventually) too.
+Worse, we can't test the things we don't think of, or don't know about; we're vulnerable to our limited knowledge, the availability heuristic, confirmation bias, and so on. In fact, we humans are generally ill equipped for logical reasoning, even if trained.
+Humans and Reasoning
+A Toy Example
+Suppose we're thinking about the workings of a small company. We're given some facts about the company, and have to answer a question based on those facts. Here's an example. We know that:
+-
+
- Alice supervises Bob. +
- Bob supervises Charlie. +
- Alice graduated Brown. +
- Charlie graduated Harvale. +
Question: Does someone who graduated from Brown directly supervise someone who graduated from another University?
+
+
+Think, then click.
+Yes! Regardless of whether Bob graduated from Brown, some Brown graduate supervises some non-Brown graduate. Reasoning by hypotheticals, there is one fact we don't know: where Bob graduated. In case he graduated Brown, he supervises Charlie, a non-Brown graduate. In case he graduated from another school, he's supervised by Alice, a Brown graduate.
+Humans tend to be very bad at reasoning by hypotheticals. There's a temptation to think that this puzzle isn't solvable because we don't know where Bob graduated from. Even Tim thought this at first after seeing the puzzle—in grad school! For logic!
+Now imagine a puzzle with a thousand of these unknowns. A thousand boolean variables means cases to reason through. Want to use a computer yet?
+ +Of course, this isn't really about logic puzzles.
+A Real Scenario
+There's a real cryptographic protocol called the Needham-Schroeder public-key protocol. You can read about it here. Unfortunately the protocol has a bug: it's vulnerable to attack if one of the principles can be fooled into starting an exchange with a badly-behaved or compromised agent. We won't go into specifics. Instead, let's focus on the fact that it's quite easy to get things like protocols wrong, and sometimes challenging for us humans to completely explore all possible behaviors -- especially since there might be behaviors we'd never even considered! It sure would be nice if we could get a computer to help out with that.
+A pair of former 1710 students did an ISP on modeling crypto protocols, using the tools you'll learn in class. Here's an example picture, generated by their model, of the flaw in the Needham-Schroeder protocol:
+
You don't need to understand the specifics of the visualization; the point is that someone who has studied crypto protocols would. And this really does show the classic attack on Needham-Schroeder. You may not be a crypto-protocol person, but you probably are an expert in something you'd like to model, and you might very well get the chance to do so this semester.
+Automated Reasoning as an Assistive Device
+The human species has been so successful, in part, because of our ability to use assistive devices—tools! Eyeglasses, bicycles, hammers, bridges: all devices that assist us in navigating the world in our fragile meat-bodies. One of our oldest inventions, writing, is an assistive device that increases our long-term memory space and makes that memory persistent. Computers are only one in a long line of such inventions.
+So, naturally, we've found ways to:
+-
+
- use computers to help us test our ideas; +
- use computers to exhaustively check program correctness; +
- use computers to help us find gaps in our intuition about a program; +
- use computers to help us explore the design space of a data structure, or algorithm, card game, or chemical reaction; +
- etc. +
There's a large body of work in Computer Science that uses logic to do all those things. We tend to call it formal methods, especially when the focus is on reasoning about systems. It touches on topics like system modeling, constraint solving, program analysis, design exploration, and more. That's what this book is about: the foundational knowledge to engage with many different applications of these ideas, even if you don't end up working with them directly every day.
+More concretely, we'll focus on a class of techniques called lightweight formal methods, which are characterized by tradeoffs that favor ease of use over strong guarantees (although we'll sometimes achieve those as well).
+
+
+
+
+
+Jeanette Wing and Daniel Jackson wrote a short article coining the term "lightweight FM" in the 90's, which you can find online.
+
+
+
+
+
+When we say "systems" in this book we don't necessarily mean the kind of systems you see in a class on networks, hardware architecture, or operating systems. You can apply the techniques in this book to those subjects quite naturally, but you can also apply it to user interfaces, type systems in programming, hardware, version control systems like Git, web security, cryptographic protocols, robotics, puzzles, sports and games, and much more. So we construe the word "system" very broadly.
+Here are some examples of "systems" that students have modeled in Forge: lifetimes in Rust, network reachability, and poker!
+The Future of Computing
+For better or worse, The shape of engineering is changing. Lots of people are excited, scared, or both about large language models like ChatGPT. This book won't teach you how to use generative AI, so it's reasonable to wonder: why learn from this book, instead of another AI book?
+There are two questions that will never go out of style, and won't be answered by AI (at least, not in our lifetimes):
+-
+
- What do you want to build? What does your customer really need? Answering this requires talking to them and other stakeholders, watching their processes, seeking their feedback, and adjusting your design based on it. And no matter who (or what) is writing the actual code, you need to be able to express all this precisely enough that they (or it) can succeed at the implementation. +
- How will you evaluate what you get? No matter who (or what) is building the system, verification is needed before the system can be trusted. +
Even setting aside the customer-facing aspects, we'll still need to think critically about what it is we want and how to evaluate whether we're getting it. The skills you learn here will remain useful (or become even more so) as engineering evolves. And those skills will be useful for more than just code.
+ + +Looking Ahead: Tools
+The main tool we'll use in this course is Forge. Forge is a tool for modeling systems; we'll talk about what that means later on. For now, be aware that we'll be progressing through three language levels in Forge:
+-
+
- Froglet, which restricts the set of operations available so that we can jump right in more easily. If you have intuitions about object-oriented programming, those intuitions will be useful in Froglet, although there are a few important differences that we'll talk about. +
- Relational Forge, which expands the set of operations available to include sets, relations, and relational operators. Again, we'll cover these in detail later. They are useful for reasoning about complex relationships between objects and for representing certain domains, like databases or graphs. +
- Temporal Forge, which lets us cleanly model how a system's state evolves over time. +
We'll also use:
+-
+
- Hypothesis, a testing library for Python; and +
- Z3, an SMT solver library. +
Intro to Modeling Systems (Part 1: Tic-Tac-Toe)
+What's a Model?
+A model is a representation of a system that faithfully includes some but not all of the system's complexity. There are many different ways to model a system, all of which have different advantages and disadvantages. Think about what a car company does before it produces a new car design. Among other things, it creates multiple models. E.g.,
+-
+
- it models the car in some computer-aided design tool; and then +
- creates a physical model of the car, perhaps with clay, for testing in wind tunnels etc. +
There may be many different models of a system, all of them focused on something different. As the statisticians say, "all models are wrong, but some models are useful". Learning how to model a system is a key skill for engineers, not just within "formal methods". Abstraction is one of the key tools in Computer Science, and modeling lies at the heart of abstraction.
+In this course, the models we build aren't inert; we have tools that we can use the explore and analyze them!
+Don't Be Afraid of Imperfect Representations
+We don't need to fully model a system to be able to make useful inferences. We can simplify, omit, and abstract concepts/attributes to make models that approximate the system while preserving the fundamentals that we're interested in.
+EXERCISE: If you've studied physics, there's a great example of this in statics and dynamics. Suppose I drop a coin from the top of the science library, and ask you what its velocity will be when it hits the ground. Using the methods you learn in beginning physics, what's something you usefully disregard?
+
+
+Think, then click!
+Air resistance! Friction! We can still get a reasonable approximation for many problems without needing to include that. (And advanced physics adds even more factors that aren't worth considering at this scale.) The model without friction is often enough.
+Systems vs. Models (and Implementations)
+When we say "systems" in this module, we mean the term broadly. A distributed system (like replication in MongoDB) is a system, but so are user interfaces and hardware devices like CPUs and insulin pumps. Git is a system for version control. The web stack, cryptographic protocols, chemical reactions, the rules of sports and games---these are all systems too!
+To help build intuition, let's work with a simple system: the game of tic-tac-toe (also called noughts and crosses). There are many implementations of this game, including this one that Tim wrote for these notes in Python. And, of course, these implementations often have corresponding test suites, like this (incomplete) example.
+Exercise: Play a quick game of tic-tac-toe by hand. If you can, find a partner, but if not, then play by yourself.
+Notice what just happened. You played the game. In doing so, you ran your own mental implementation of the rules. The result you got was one of many possible games, each with its own specific sequence of legal moves, leading to a particular ending state. Maybe someone won, or maybe the game was a tie. Either way, many different games could have ended with that same board.
+Modeling is different from programming. When you're programming traditionally, you give the computer a set of instructions and it follows them. This is true whether you're programming functionally or imperatively, with or without objects, etc. Declarative modeling languages like Forge work differently. The goal of a model isn't to run instructions, but rather to describe the rules that govern systems.
+Here's a useful comparison to help reinforce the difference (with thanks to Daniel Jackson):
+-
+
- An empty program does nothing. +
- An empty model allows every behavior. +
Modeling Tic-Tac-Toe Boards
+What are the essential concepts in a game of tic-tac-toe?
+
+
+
+
+
+When we're first writing a model, we'll start with 5 steps. For each step, I'll give examples from tic-tac-toe and also for binary search trees (which we'll start modeling soon) for contrast.
+-
+
- What are the datatypes involved, and their fields?
+
-
+
- For tic-tac-toe: they might be the 3-by-3 board and the
XandOmarks that go in board locations.
+ - For a binary search tree: they might be the tree nodes and their left and right children. +
+ - For tic-tac-toe: they might be the 3-by-3 board and the
- What makes an instance of these datatypes well formed? That is, what conditions are needed for them to not be garbage?
+
-
+
- For tic-tac-toe, we might require that the indexes used are between
0and2, since the board is 3-by-3.
+ - For a binary search tree, we might require that every node has at most one left child, at most one right child, a unique parent, ... +
+ - For tic-tac-toe, we might require that the indexes used are between
- What's a small example of how these datatypes can be instantiated?
+
-
+
- For tic-tac-toe, the empty board would be an example. So would the board where
Xmoves first into the middle square.
+ - For a binary search tree, this might be a tree with only one node, or a 3-node tree where the root's left and right children are leaves. +
+ - For tic-tac-toe, the empty board would be an example. So would the board where
- What does the model look like when run?
+
-
+
- For tic-tac-toe, we should see a board with some number of
XandOmarks.
+ - For a binary search tree, we should see some set of nodes that forms a single tree via left- and right-children. +
+ - For tic-tac-toe, we should see a board with some number of
- What domain predicates are there? Well-formedness defines conditions that are needed for an instantiation to not be "garbage". But whatever we're modeling surely has domain-specific concepts of its own, which may or may not hold.
+
-
+
- For tic-tac-toe, we care a great deal if the board is a winning board or not. Similarly, we might care if it looks like someone has cheated. +
- For a binary search tree, we care if the tree is balanced, or if it satisfies the BST invariant. +
+
+
+
+
+
+Why make this distinction between well-formedness and domain predicates? Because one should always hold in any instance Forge considers, but the other may or may not hold. In fact, we might want to use Forge to verify that a domain predicate always holds! And if we've told Forge that any instance that doesn't satisfy it is garbage, Forge won't find us such an instance.
+Datatypes
+We might list:
+-
+
- the players
XandO;
+ - the 3-by-3 game board, where players can put their marks; +
- the idea of whose turn it is at any given time; and +
- the idea of who has won the game at any given time. +
Now let's add those ideas to a model in Forge!
+#lang forge/froglet
+The first line of any Forge model will be a #lang line, which says which Forge language the file uses. We'll start with the Froglet language for now. Everything you learn in this language will apply in other Forge languages, so I'll use "Forge" interchangeably.
Now we need a way to talk about the noughts and crosses themselves. So let's add a sig that represents them:
#lang forge/froglet
+abstract sig Player {}
+one sig X, O extends Player {}
+You can think of sig in Forge as declaring a kind of object. A sig can extend another, in which case we say that it is a child of its parent, and child sigs cannot overlap. When a sig is abstract, any member must also be a member of one of that sig's children; in this case, any Player must either be X or O. Finally, a one sig has exactly one member---there's only a single X and O in our model.
We also need a way to represent the game board. We have a few options here: we could create an Index sig, and encode an ordering on those (something like "column A, then column B, then column C"). Another is to use Forge's integer support. Both solutions have their pros and cons. Let's use integers, in part to get some practice with them.
#lang forge/froglet
+abstract sig Player {}
+one sig X, O extends Player {}
+
+sig Board {
+ board: pfunc Int -> Int -> Player
+}
+Every Board object contains a board field describing the moves made so far. This field is a partial function, or dictionary, for every Board that maps each (Int, Int) pair to at most one Player.
Well-formedness
+These definitions sketch the overall shape of a board: players, marks on the board, and so on. But not all boards that fit the definition will be valid. For example:
+-
+
- Forge integers aren't true mathematical integers, but are bounded by a bitwidth we give whenever we run the tool. So we need to be careful here. We want a classical 3-by-3 board with indexes of (say)
0,1, and2, not a board where (e.g.) row-5, column-1is a valid location.
+
We'll call these well-formedness constraints. They aren't innately enforced by our sig declarations, but we'll almost always want Forge to enforce them, so that it doesn't find "garbage instances". Let's write a wellformedness predicate:
-- a Board is well-formed if and only if:
+pred wellformed[b: Board] {
+ -- row and column numbers used are between 0 and 2, inclusive
+ all row, col: Int | {
+ (row < 0 or row > 2 or col < 0 or col > 2)
+ implies no b.board[row][col]
+ }
+}
+This predicate is true of any Board if and only if the above 2 constraints are satisfied. Let's break down the syntax:
-
+
- Constraints can quantify over a domain. E.g.,
all row, col: Int | ...says that for any pair of integers (up to the given bidwidth), the following condition (...) must hold. Forge also supports, e.g., existential quantification (some), but we don't need that yet. We also have access to standard boolean operators likeor,implies, etc.
+ - Formulas in Forge always evaluate to a boolean; expressions evaluate to sets. For example,
+
-
+
- the expression
b.board[row][col]evaluates to thePlayer(if any) with a mark at location (row,col) in boardb; but
+ - the formula
no b.board[row][col]is true if and only if there is no such `Player``.
+
+ - the expression
- A
pred(predicate) in Forge is a helper function that evaluates to a boolean. Thus, its body should always be a formula.
+
+
+
+
+
+Notice that, rather than describing a process that produces a well-formed board, or even instructions to check well-formedness, we've just given a declarative description of what's necessary and sufficient for a board to be well-formed. If we'd left the predicate body empty, any board would be considered well-formed---there'd be no formulas to enforce!
+A Few Examples
+Since a predicate is just a function that returns true or false, depending on its arguments and whichever instance Forge is looking at, we can write tests for it the same way we would for any other boolean-valued function. But even if we're not testing, it can be useful to write a small number of examples, so we can build intuition for what the predicate means.
+We'll write two examples in Forge:
+-- Helper to make these examples easier to write
+pred all_wellformed { all b: Board | wellformed[b]}
+
+-- all_wellformed should be _true_ for the following instance
+example firstRowX_wellformed is {all_wellformed} for {
+ Board = `Board0 -- backquote labels atoms
+ X = `X O = `O -- examples must define all sigs
+ Player = X + O
+ `Board0.board = (0, 0) -> `X + -- examples must define all fields
+ (0, 1) -> `X + -- here, the partial function for
+ (0, 2) -> `X -- the board (empty squares remain empty)
+}
+
+-- all_wellformed should be _false_ for the following instance
+example off_board_not_wellformed is {not all_wellformed} for {
+ Board = `Board0
+ X = `X O = `O
+ Player = X + O
+ `Board0.board = (-1, 0) -> `X +
+ (0, 1) -> `X +
+ (0, 2) -> `X
+}
+In Forge, examples are automatically run whenever your model executes. They describe basic intent about a given predicate; in this case, we're testing that a board where X has moved 3 times in valid locations is considered well formed. In contrast, if X has moved in an invalid location, it won't be considered well formed. Again, we're not making judgements about the rules being obeyed yet—just about whether our model is conforming to how we've encoded the game, using 0, 1, and 2 as the only valid indexes.
+
+
+
+
+Notice that we've got a test thats a positive example and another test that's a negative example. We want to make sure to exercise both cases, or else "always true" or "always" false could pass our suite.
+Running Forge
+The run command tells Forge to search for an instance satisfying the given constraints:
run { some b: Board | wellformed[b]}
+When we click the play button in the VSCode extension, the engine solves the constraints and produces a satisfying instance, (Because of differences across solver versions, hardware, etc., it's possible you'll see a different instance than the one shown here.) A browser window should pop up with a visualization. You can also run racket <filename.frg> in the terminal, although we recommend the VSCode extension.
+
+
+
+
+If you're running on Windows, the Windows-native cmd and PowerShell terminals will not properly load Forge's visualizer. Instead, we suggest using one of many other options on Windows that we've tested and know to work: the VSCode extension (available on the VSCode Marketplace), DrRacket, Git bash, Windows Subsystem for Linux, or Cygwin.
+
There are many options for visualization. The default which loads initially is a directed-graph based one:
+This isn't very useful; it looks nothing like a tic-tac-toe board! We can make more progress by using the "Table" visualization---which isn't ideal either:
+Forge also allows users to make custom visualizations via short JavaScript programs; here's an example basic visualizer for this specific tic-tac-toe model that produces images like this one:
+We'll talk more about visualization scripts later. For now, let's proceed. TODO: replace img with one matching the table view +TODO: add side-by-side CSS
++
This instance contains a single board, and it has 9 entries. Player O has moved in all of them (the 0 suffix of O0 in the display is an artifact of how Forge's engine works; ignore it for now). It's worth noticing two things:
-
+
- This board doesn't look quite right: player
Ooccupies all the squares. We might ask: has playerObeen cheating? But the fact is that this board satisfies the constraints we have written so far. Forge produces it simply because our model isn't yet restrictive enough, and for no other reason. "Cheating" doesn't exist yet.
+ - We didn't say how to find that instance. We just said what we wanted, and the tool performed some kind of search to find it. So far the objects are simple, and the constraints basic, but hopefully the power of the idea is coming into focus. +
Reflection: Implementation vs. Model
+So far we've just modeled boards, not full games. But we can still contrast our work here against the implementation of tic-tac-toe shared above. We might ask:
+-
+
- How do the data-structure choices, and type declarations, in the implementation compare with the model? +
- Is there an implementation that matches what we just did? (The program's purpose isn't to generate boards, but to play games!) +
Domain Predicates
+Now let's write predicates that describe important ideas in the domain. What's important in the game of tic-tac-toe? Here are a few things.
+Starting Boards
+What would it mean to be a starting state in a game? The board is empty:
+pred starting[s: Board] {
+ all row, col: Int |
+ no s.board[row][col]
+}
+Turns
+How do we tell when it's a given player's turn? It's X's turn when there are the same number of each mark on the board:
pred XTurn[s: Board] {
+ #{row, col: Int | s.board[row][col] = X} =
+ #{row, col: Int | s.board[row][col] = O}
+}
+The {row, col: Int | ...} syntax means a set comprehension, and describes the set of row-column pairs where the board contains X (or O). The # operator gives the size of these sets, which we then compare.
Question: Is it enough to say that OTurn is the negation of XTurn?
+
+Think, then click!
+No! At least not in the model as currently written. If you're curious to see why, run the model and look at the instances produced. Instead, we need to say something like this:
+pred OTurn[s: Board] {
+ #{row, col: Int | s.board[row][col] = X} =
+ add[#{row, col: Int | s.board[row][col] = O}, 1]
+}
+
+
+
+
+
+Forge supports arithmetic operations on integers like add. While it doesn't matter for this model yet, addition (and other operations) can overflow according to 2's complement arithmetic. For example, if we're working with 4-bit integers, then add[7,1] will be -8. You can experiment with this in the visualizer's evaluator, which we'll be using a lot after the initial modeling tour is done.
+
+
+
+
+Don't try to use + for addition in any Forge language. Use add instead; this is because + is reserved for something else (which we'll explain later).
Winning the Game
+What does it mean to win? A player has won on a given board if:
+-
+
- they have placed their mark in all 3 columns of a row; +
- they have placed their mark in all 3 rows of a column; or +
- they have placed their mark in all 3 squares of a diagonal. +
We'll express this in a winner predicate that takes the current board and a player name. Let's also define a couple helper predicates along the way:
pred winRow[s: Board, p: Player] {
+ -- note we cannot use `all` here because there are more Ints
+ some row: Int | {
+ s.board[row][0] = p
+ s.board[row][1] = p
+ s.board[row][2] = p
+ }
+}
+
+pred winCol[s: Board, p: Player] {
+ some column: Int | {
+ s.board[0][column] = p
+ s.board[1][column] = p
+ s.board[2][column] = p
+ }
+}
+
+pred winner[s: Board, p: Player] {
+ winRow[s, p]
+ or
+ winCol[s, p]
+ or
+ {
+ s.board[0][0] = p
+ s.board[1][1] = p
+ s.board[2][2] = p
+ } or {
+ s.board[0][2] = p
+ s.board[1][1] = p
+ s.board[2][0] = p
+ }
+}
+After writing these domain predicates, we're reaching a fairly complete model for a single tic-tac-toe board. Let's decide how to fix the issue we saw above (the reason why OTurn couldn't be the negation of XTurn): perhaps a player has moved too often.
Should we add something like OTurn[s] or XTurn[s] to our wellformedness predicate? No! If we then later enforced wellformedness for all boards, that would exclude "cheating" instances where a player has more moves on the board than are allowed. But this has some risk, depending on how we intend to use the wellformed predicate:
-
+
- If we were only ever generating valid boards, a cheating state might well be spurious, or at least undesirable. In that case, we might prevent such states in
wellformedand rule it out.
+ - If we were generating arbitrary (not necessarily valid) boards, being able to see a cheating state might be useful. In that case, we'd leave it out of
wellformed.
+ - If we're interested in verification, e.g., we are asking whether the game of Tic-Tac-Toe enables ever reaching a cheating board, we shouldn't add
not cheatingtowellformed; becausewellformedalso excludes garbage boards, we'd probably use it in our verification—in which case, Forge will never find us a counterexample!
+
[TODO: move this point to position it properly, if PBT comes after vs. before]
+
+
+
+
+
+Notice the similarity between this issue and what we do in property-based testing. Here, we're forced to distinguish between what a reasonable board is (analogous to the generator's output in PBT) and what a reasonable behavior is (analogous to the validity predicate in PBT). One narrows the scope of possible worlds to avoid true "garbage"; the other checks whether the system behaves as expected in one of those worlds.
+We'll come back to this later, when we've had a bit more modeling experience. For now, let's separate our goal into a new predicate called balanced, and add it to our run command above:
pred balanced[s: Board] {
+ XTurn[s] or OTurn[s]
+}
+run { some b: Board | wellformed[b] and balanced[b]}
+If we click the "Next" button a few times, we see that not all is well: we're getting boards where wellformed is violated (e.g., entries at negative rows, or multiple moves in one square).
We're getting this because of how the run was phrased. We said to find an instance where some board was well-formed and valid, not one where all boards were. By default, Forge will find instances with up to 4 Boards. So we can fix the problem either by telling Forge to find instances with only 1 Board:
run { some b: Board | wellformed[b] and balanced[b]}
+for exactly 1 Board
+or by saying that all boards must be well-formed and balanced:
+run { all b: Board | wellformed[b] and balanced[b]}
+Practice with run
+The run command can be used to give Forge more detailed instructions for its search.
No Boards
+Is it possible for an instance with no boards to still satisfy constraints like these?
+run {
+ all b: Board | {
+ -- X has won, and the board looks OK
+ wellformed[b]
+ winner[b, X]
+ balanced[b]
+ }
+ }
+
+
+Think, then click!
+Yes! There aren't any boards, so there's no obligation for anything to satisfy the constraints inside the quantifier. You can think of the all as something like a for loop in Java or the all() function in Python: it checks every Board in the instance. If there aren't any, there's nothing to check—return true.
Adding More
+This addition also requires that X moved in the middle of the board:
run {
+ all b: Board | {
+ -- X has won, and the board looks OK
+ wellformed[b]
+ winner[b, X]
+ balanced[b]
+ -- X started in the middle
+ b.board[1][1] = X
+ }
+ } for exactly 2 Board
+Notice that, because we said exactly 2 Board here, Forge must find instances containing 2 tic-tac-toe boards, and both of them must satisfy the constraints: wellformedness, X moving in the middle, etc. You could ask for a board where X hasn't won by adding not winner[b, X].
Intro to Modeling Systems (Part 2: BSTs)
+Now that we've written our first model—tic-tac-toe boards—let's switch to something a bit more serious: binary search trees. A binary search tree (BST) with an added property about its structure. So let's start modeling by following the our 5-step process.
+Datatypes
+A binary tree is made up of nodes:
+#lang forge/froglet
+sig Node {
+ key: one Int, -- every node has some key
+ left: lone Node, -- every node has at most one left-child
+ right: lone Node -- every node has at most one right-child
+}
+Wellformedness
+What makes a binary tree a binary tree? One way to say it is:
+-
+
- it's tree-shaped: there are no cycles and nodes have at most one parent node; and +
- it's connected, that is, it's a tree and not a forest. +
Let's get started encoding this. Sometimes it can be helpful to write a domain predicate along with wellformedness, if it makes the model more clear, hence why we wrote root:
#lang forge/froglet
+sig Node {
+ key: one Int, -- every node has some key
+ left: lone Node, -- every node has at most one left-child
+ right: lone Node -- every node has at most one right-child
+}
+
+pred root[n: Node] {
+ -- a node is a root if it has no ancestor (note this doesn't enforce uniqueness)
+ no n2: Node | n = n2.left or n = n2.right
+}
+
+pred wellformed {
+ -- no cycles: no node can reach itself via a succession of left and right fields
+ all n: Node | not reachable[n, n, left, right]
+
+ -- all non-root nodes have a common ancestor from which both are reachable
+ -- the "disj" keyword means that n1 and n2 must be _different_
+ all disj n1, n2: Node | (not root[n1] and not root[n2]) implies {
+ some anc: Node | reachable[n1, anc, left, right] and
+ reachable[n2, anc, left, right] }
+
+ -- nodes have a unique parent (if any)
+ all disj n1, n2, n3: Node |
+ not ((n1.left = n3 or n1.right = n3) and (n2.left = n3 or n2.right = n3))
+
+}
+Write an example or two
+[FILL: example trees: singleton, empty, unbalanced...]
+View some instances
+-- View a tree or two
+run {binary_tree} for exactly 8 Node
+[FILL: Oops, not quite right, we were missing a constraint; underconstraint bug -- fix it]
+Missing:
+ -- left+right differ (unless both are empty)
+ all n: Node | some n.left => n.left != n.right
+FILL: and iterate.
+Going further
+-- Run a test: our predicate enforces a unique root exists (if any node exists)
+pred req_unique_root {
+ no Node or {
+ one root: Node |
+ all other: Node-root | other in descendantsOf[root]}}
+assert binary_tree is sufficient for req_unique_root for 5 Node
+From Boards to Games
+What do you think a game of tic-tac-toe looks like? How should we model the moves between board states?
+
+
+Think, then click!
+It's often convenient to think of the game as a big graph, where the nodes are the states (possible board configurations) and the edges are transitions (in this case, legal moves of the game). Here's a rough sketch:
+
+
A game of tic-tac-toe is a sequence of steps in this graph, starting from the empty board. Let's model it.
+First, what does a move look like? A player puts their mark at a specific location. In Alloy, we'll represent this using a transition predicate: a predicate that says when it's legal for one state to evolve into another. We'll often call these the pre-state and post-state of the transition:
+pred move[pre: Board, row: Int, col: Int, p: Player, post: Board] {
+ // ...
+}
+What constraints should we add? It's useful to divide the contents of such a predicate into:
+-
+
- a guard, which allows the move only if the pre-state is suitable; and +
- an action, which defines what is in the post-state based on the pre-state and the move parameters. +
For the guard, in order for the move to be valid, it must hold that in the pre-state:
+-
+
- nobody has already moved at the target location; and +
- it's the moving player's turn. +
For the action:
+-
+
- the new board is the same as the old, except for the addition of the player's mark at the target location. +
Now we can fill in the predicate. Let's try something like this:
+pred move[pre: Board, row: Int, col: Int, p: Player, post: Board] {
+ -- guard:
+ no pre.board[row][col] -- nobody's moved there yet
+ p = X implies XTurn[pre] -- appropriate turn
+ p = O implies OTurn[pre]
+
+ -- action:
+ post.board[row][col] = p
+ all row2: Int, col2: Int | (row!=row2 and col!=col2) implies {
+ post.board[row2][col2] = pre.board[row2][col2]
+ }
+}
+There are many ways to write this predicate. However, we're going to stick with this form because it calls out an important point. Suppose we had only written post.board[row][col] = p for the action, without the all on the next following lines. Those added lines, which we'll call a frame condition, say that all other squares remain unchanged; without them, the contents of any other square might change in any way. Leaving them out would cause an underconstraint bug: the predicate would be too weak to accurately describe moves in tic-tac-toe.
Exercise: comment out the 3 frame-condition lines and run the model. Do you see moves where the other 8 squares change arbitrarily?
+Exercise: could there be a bug in this predicate? (Run Forge and find out!)
+
+
+
+
+Think, then click
+The all row2... formula says that for any board location where both the row and column differ from the move's, the board remains the same. But is that what we really wanted? Suppose X moves at location 1, 1. Then of the 9 locations, which is actually protected?
| Row | Column | Protected? |
|---|---|---|
| 0 | 0 | yes |
| 0 | 1 | no (column 1 = column 1) |
| 0 | 2 | yes |
| 1 | 0 | no (row 1 = row 1) |
| 1 | 1 | no (as intended) |
| 1 | 2 | no (row 1 = row 1) |
| 2 | 0 | yes |
| 2 | 1 | no (column 1 = column 1) |
| 2 | 2 | yes |
Our frame condition was too weak! We need to have it take effect whenever either the row or column is different. Something like this will work:
+ all row2: Int, col2: Int |
+ ((row2 != row) or (col2 != col)) implies {
+ post.board[row2][col2] = pre.board[row2][col2]
+ }
+
+A Simple Property
+Once someone wins a game, does their win still persist, even if more moves are made? I'd like to think so: moves never get undone, and in our model winning just means the existence of 3-in-a-row for some player. We probably even believe this property without checking it. However, it won't always be so straightforward to show that properties are preserved by the system. We'll check this one in Forge as an example of how you might prove something similar in a more complex system.
+
+
+
+
+
+This is our first step into the world of verification. Asking whether or not a program, algorithm, or other system always satisfies some assertion is a core problem in formal methods, and has a long and storied history.
+We'll tell Forge to find us pairs of states, connected by a move: the pre-state before the move, and the post-state after it. That's any potential transition in tic-tac-toe. The trick is in adding two more constraints. We'll say that someone has won in the pre-state, but they haven't won in the post-state.
+pred winningPreservedCounterexample {
+ some pre, post: Board | {
+ some row, col: Int, p: Player |
+ move[pre, post, row, col, p]
+ winner[pre, X]
+ not winner[post, X]
+ }
+}
+run {
+ all s: Board | wellformed[s]
+ winningPreservedCounterexample
+}
+The check passes---Forge can't find any counterexamples. We'll see this reported as "UNSAT" in the visualizer.
+ +Generating Complete Games
+Recall that our worldview for this model is that systems transition between states, and thus we can think of a system as a directed graph. If the transitions have arguments, we'll sometimes label the edges of the graph with those arguments. This view is sometimes called a discrete event model, because one event happens at a time. Here, the events are moves of the game. In a bigger model, there might be many different types of events.
+TODO: I think this goes later in the book, we don't want to start on finite traces yet.
+Today, we'll ask Forge to find us traces of the system, starting from an initial state. We'll also add a Game sig to incorporate some metadata.
one sig Game {
+ initialState: one Board,
+ next: pfunc Board -> Board
+}
+
+pred traces {
+ -- The trace starts with an initial state
+ starting[Game.initialState]
+ no sprev: Board | Game.next[sprev] = Game.initialState
+ -- Every transition is a valid move
+ all s: Board | some Game.next[s] implies {
+ some row, col: Int, p: Player |
+ move[s, row, col, p, Game.next[s]]
+ }
+}
+By itself, this wouldn't be quite enough; we might see a bunch of disjoint traces. We could add more constraints manually, but there's a better option: tell Forge, at runtime, that next represents a linear ordering on states.
run {
+ traces
+} for {next is linear}
+The key thing to notice here is that next is linear isn't a constraint; it's a separate annotation given to Forge alongside a run or a test. Never put such an annotation in a constraint block; Forge won't understand it. These annotations narrow Forge's bounds (the space of possible worlds to check) which means they can often make problems more efficient for Forge to solve.
In general, Forge accepts such annotations after numeric bounds. E.g., if we wanted to see full games, rather than unfinished game prefixes (the default bound on any sig, including Board, is up to 4) we could have asked:
run {
+ traces
+} for exactly 10 Board for {next is linear}
+You might notice that because of this, some traces are excluded. That's because next is linear forces exact bounds on Board. More on this next time.
The Evaluator
+Moreover, since we're now viewing a single fixed instance, we can evaluate Forge expressions in it. This is great for debugging, but also for just understanding Forge a little bit better. Open the evaluator here at the bottom of the right-side tray, under theming. Then enter an expression or constraint here:
+
Type in something like some s: State | winner[s, X]. Forge should give you either #t (for true) or #f (for false) depending on whether the game shows X winning the game.
Optimizing
+You might notice that this model takes a while to run, after we start reasoning about full games. Why might that be? Let's re-examine our bounds and see if there's anything we can adjust. In particular, here's what the evaluator says we've got for integers:
+
Wow---wait, do we really need to be able to count up to 7 for this model? Probably not. If we change our integer bounds to 3 Int we'll still be able to use 0, 1, and 2, and the search space is much smaller.
Anticipated Questions
+TODO: much of this should be moved later
+A Visual Sketch of How Forge Searches
+Suppose we're using Forge to search for family trees. There are infinitely many potential family tree instances, but Forge needs to work with a finite search space. This is where the bounds of a run come in; they limit the set of instances Forge will even consider. Constraints you write are not yet involved at this point.
Once the bounded search space has been established, Forge uses the constraints you write to find satisfying instances within the bounded search space.
+
The engine uses bounds and constraints very differently, and inferring constraints is often less efficient than inferring bounds. But the engine treats them differently, which means sometimes the distinction leaks through.
+"Nulls" in Forge
+In Forge, there is a special value called none. It's analogous (but not the same!) to a null in languages like Java.
Suppose I added this predicate to our run command in the tic-tac-toe model:
pred myIdea {
+ all row1, col1, row2, col2: Int |
+ (row1 != row2 or col1 != col2) implies
+ Game.initialState.board[row1][col1] !=
+ Game.initialState.board[row2][col2]
+}
+I'm trying to express that every entry in the board is different. This should easily be true about the initial board, as there are no pieces there.
+For context, recall that we had defined a Game sig earlier:
one sig Game {
+ initialState: one State,
+ nextState: pfunc State -> State
+}
+What do you think would happen?
+
+
+Think (or try it in Forge) then click!
+It's very likely this predicate would be unsatisfiable, given the constraints on the initial state. Why?
+Because none equals itself! We can check this:
test expect {
+ nullity: {none != none} is unsat
+}
+Thus, when you're writing constraints like the above, you need to watch out for none: the value for every cell in the initial board is equal to the value for every other cell!
+
+
+
+
+The none value in Forge has at least one more subtlety: none is "reachable" from everything if you're using the built-in reachable helper predicate. That has an impact even if we don't use none explicitly. If I write something like: reachable[p.spouse, Nim, parent1, parent2] I'm asking whether, for some person p, their spouse is an ancestor of Nim. If p doesn't have a spouse, then p.spouse is none, and so this predicate would yield true for p.
Some as a Quantifier Versus Some as a Multiplicity
+The keyword some is used in 2 different ways in Forge:
-
+
- it's a quantifier, as in
some b: Board, p: Player | winner[s, p], which says that somebody has won in some board; and
+ - it's a multiplicity operator, as in
some Game.initialState.board[1][1], which says that that cell of the initial board is populated.
+
Implies vs. Such That
+You can read some row : Int | ... as "There exists some integer row such that ...". The transliteration isn't quite as nice for all; it's better to read all row : Int | ... as "In all integer rows, it holds that ...".
If you want to further restrict the values used in an all, you'd use implies. But if you want to add additional requirements for a some, you'd use and. Here are 2 examples:
-
+
- All: "Everybody who has a
parent1doesn't also have that person as theirparent2":all p: Person | some p.parent1 implies p.parent1 != p.parent2.
+ - Some: "There exists someone who has a
parent1and aspouse":some p: Person | some p.parent1 and some p.spouse.
+
Technical aside: The type designation on the variable can be interpreted as having a character similar to these add-ons: and (for some) and implies (for all). E.g., "there exists some row such that row is an integer and ...", or "In all rows, if row is an integer, it holds that...".
There Exists some Atom vs. Some Instance
+Forge searches for instances that satisfy the constraints you give it. Every run in Forge is about satisfiability; answering the question "Does there exist an instance, such that...".
Crucially, you cannot write a Forge constraint that quantifies over instances themselves. You can ask Forge "does there exist an instance such that...", which is pretty flexible on its own. E.g., if you want to check that something holds of all instances, you can ask Forge to find counterexamples. This is how assert ... is necessary for ... is implemented, and how the examples from last week worked.
One Versus Some
+The one quantifier is for saying "there exists a UNIQUE ...". As a result, there are hidden constraints embedded into its use. one x: A | myPred[x] really means, roughly, some x: A | myPred[x] and all x2: A | not myPred[x]. This means that interleaving one with other quantifiers can be subtle; for that reason, we won't use it except for very simple constraints.
If you use quantifiers other than some and all, beware. They're convenient, but various issues can arise.
Testing Predicate Equivalence
+Checking whether or not two predicates are equivalent is the core of quite a few Forge applications---and a great debugging technique sometimes.
+How do you do it? Like this:
+pred myPred1 {
+ some i1, i2: Int | i1 = i2
+}
+pred myPred2 {
+ not all i2, i1: Int | i1 != i2
+}
+assert myPred1 is necessary for myPred2
+assert myPred2 is necessary for myPred1
+If you get an instance where the two predicates aren't equivalent, you can use the Sterling evaluator to find out why. Try different subexpressions, discover which is producing an unexpected result! E.g., if we had written (forgetting the not):
pred myPred2 {
+ all i2, i1: Int | i1 != i2
+}
+One of the assertions would fail, yielding an instance in Sterling you could use the evaluator with.
+More Testing Syntax and a Lesson
+I'm not going to use this syntax in class if I don't need to, because it's less intentional. But using it here lets me highlight a common conceptual issue with Forge in general.
+test expect {
+ -- correct: "no counterexample exists"
+ p1eqp2_A: {
+ not (myPred1 iff myPred2)
+ } is unsat
+ -- incorrect: "it's possible to satisfy what i think always holds"
+ p1eqp2_B: {
+ myPred1 iff myPred2
+ } is sat
+
+}
+These two tests do not express the same thing! One asks Forge to find an instance where the predicates are not equivalent (this is what we want). The other asks Forge to find an instance where they are equivalent (this is what we're hoping holds for any instance, not just one)!
+ +