This gist shows an example of how you can use HTML and CSS to lay out trees used for axiomatic proofs of correctness for your code. The example used here is the While language, as defined in the Nielson and Nielson book Semantics with Applications.
Last active
May 13, 2018 11:12
-
-
Save c-harding/17a522bbe287af896c9851de7ee1a018 to your computer and use it in GitHub Desktop.
Axiomatic Tree Proof Formatting
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| <!DOCTYPE html> | |
| <html> | |
| <head> | |
| <link rel="stylesheet" href="axiomatic.css"> | |
| <title>Exploring the axiomatic semantics of array access</title> | |
| </head> | |
| <body> | |
| <h1>Exploring the axiomatic semantics of array access for the While language</h1> | |
| <cite>Charlie Harding</cite> | |
| <p>The following is based on <a href="axiomatic.html">the axiomatic semantic rules for the While language</a>.</p> | |
| <h2>Assignment</h2> | |
| <p>The following is the rule proposed for assignment as per <i>Nielson and Nielson</i>.</p> | |
| <axiom> | |
| <stm><rule>ASSN</rule><cond>P<update><syntax>x</syntax><aval>a</aval></update></cond>x := a<cond>P</cond></stm> | |
| </axiom> | |
| <h3>Example</h3> | |
| <axiom> | |
| <axiom> | |
| <axiom> | |
| <stm><rule>ASSN</rule><cond><aval>(y = 12) ? 5 : 7</aval> = 5</cond>x := (y = 12) ? 5 : 7<cond><aval>x</aval> = 5</cond></stm> | |
| </axiom> | |
| <stm><rule>CONS</rule><cond><ternary><div><span>5</span><span><aval>y</aval> = 12</span></div><div><span>7</span><span>otherwise</span></div></ternary> = 5</cond>x := (y = 12) ? 5 : 7<cond><aval>x</aval> = 5</cond></stm> | |
| </axiom> | |
| <stm> | |
| <rule>CONS</rule> | |
| <cond><aval>y</aval> = 12</cond>x := (y = 12) ? 5 : 7<cond><aval>x</aval> = 5</cond> | |
| </stm> | |
| </axiom> | |
| <p>Note that the CONS rule has been split in two, to make clear the derivation process.</p> | |
| <h2>Array Assignment</h2> | |
| <p>I propose the following rule for array assignment:</p> | |
| <axiom> | |
| <stm><rule>ARRA</rule><cond>P<update><listval><syntax>x</syntax><aval>a₁</aval></listval><aval>a₂</aval></update></cond>x[a₁] := a₂<cond>P</cond></stm> | |
| </axiom> | |
| <p>where <aval>arr[x]</aval> resolves to <listval><syntax>arr</syntax><aval>x</aval></listval>. This in turn could, for example, resolve to <aval><text>“</text>arr;<text>” concatenated with str(<aval>x</aval>)</text></aval>, where str is the string representation of a number, but such a definition is not needed for this exercise.</p> | |
| <h3>Example</h3> | |
| <axiom> | |
| <axiom> | |
| <axiom> | |
| <stm> | |
| <rule>ARRA</rule> | |
| <cond><aval>x</aval> = <aval>y</aval> <and/> 5 = 5</cond>arr[y] := 5<cond><aval>x</aval> = <aval>y</aval> <and/> <listval><syntax>arr</syntax><aval>y</aval></listval> = 5</cond></stm> | |
| </axiom> | |
| <stm> | |
| <rule>COND</rule> | |
| <cond><aval>x</aval> = <aval>y</aval> <and/> 5 = 5</cond>arr[y] := 5<cond><listval><syntax>arr</syntax><aval>x</aval></listval> = 5</cond></stm> | |
| </axiom> | |
| <stm> | |
| <rule>CONS</rule> | |
| <cond><aval>x</aval> = <aval>y</aval></cond>arr[y] := 5<cond><aval>arr[x]</aval> = 5</cond> | |
| </stm> | |
| </axiom> | |
| <p>My concern with this approach, however, is that the onus of converting array accesses has to be on the right-hand side, rather than the left-hand side. It also seems a bit strange that <aval>arr[x]</aval> occurs as the consequent from <listval><syntax>arr</syntax><aval>x</aval></listval>, rather than the other way around, but I presume this is because the condition involves a lot of syntax.</p> | |
| </body> | |
| </html> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| @charset "UTF-8"; | |
| axiom { | |
| display: inline-block; | |
| text-align: center; | |
| margin: 1em 10px; | |
| font-size: 1rem; } | |
| axiom axiom { | |
| margin: 0 10px; } | |
| text { | |
| font: initial; | |
| color: initial; | |
| display: inline; } | |
| and::before { | |
| content: '∧'; | |
| font-style: normal; } | |
| or::before { | |
| content: '∨'; | |
| font-style: normal; } | |
| syntax, aval { | |
| font-family: 'Fira Code', monospace; | |
| font-style: normal; | |
| color: green; } | |
| aval::before { | |
| font-family: serif; | |
| color: black; | |
| font-style: normal; | |
| content: "𝒜 ⟦"; } | |
| aval::after { | |
| font-family: serif; | |
| color: black; | |
| font-style: normal; | |
| content: "⟧"; } | |
| listval::before { | |
| font-family: serif; | |
| color: black; | |
| font-style: normal; | |
| content: "ℒ ⟦"; } | |
| listval::after { | |
| font-family: serif; | |
| color: black; | |
| font-style: normal; | |
| content: "⟧"; } | |
| listval > :not(:last-child)::after { | |
| font-family: serif; | |
| color: black; | |
| font-style: normal; | |
| content: ', '; } | |
| update { | |
| font-family: serif; | |
| color: black; | |
| font-style: normal; | |
| font-style: italic; | |
| font-size: 0.9em; } | |
| update::before { | |
| font-family: serif; | |
| color: black; | |
| font-style: normal; | |
| content: ' ['; | |
| font-size: 1.1em; } | |
| update::after { | |
| font-family: serif; | |
| color: black; | |
| font-style: normal; | |
| content: ']'; | |
| font-size: 1.1em; } | |
| update > :first-child::after { | |
| content: ' ↦ '; | |
| color: black; } | |
| update > listval:first-child::after { | |
| font-family: serif; | |
| color: black; | |
| font-style: normal; | |
| content: '⟧ ↦ '; } | |
| given, stm { | |
| font-family: 'Fira Code', monospace; | |
| font-style: normal; | |
| color: green; | |
| display: block; | |
| padding: 5px; } | |
| stm { | |
| border-top: 1px solid black; | |
| position: relative; | |
| padding-right: 2em; } | |
| rule { | |
| position: absolute; | |
| right: 0; | |
| top: 0.1em; | |
| color: black; | |
| font-family: monospace; | |
| font-size: 0.8em; } | |
| ternary { | |
| display: inline-table; | |
| position: relative; | |
| padding: 0 1em; | |
| font-size: 0.8em; | |
| vertical-align: middle; } | |
| ternary > * { | |
| display: table-row; } | |
| ternary > * > * { | |
| display: table-cell; } | |
| ternary > * > *:first-child { | |
| padding-right: 1em; } | |
| ternary::before { | |
| display: block; | |
| position: absolute; | |
| top: 0; | |
| left: 0; | |
| content: '{'; | |
| font-size: 2em; | |
| font-style: normal; } | |
| ternary::after { | |
| display: block; | |
| position: absolute; | |
| top: 0; | |
| right: 0; | |
| content: '}'; | |
| font-size: 2em; | |
| font-style: normal; } | |
| cond { | |
| font-family: serif; | |
| color: black; | |
| font-style: normal; | |
| font-style: italic; | |
| display: inline; } | |
| cond::before { | |
| font-family: serif; | |
| color: black; | |
| font-style: normal; | |
| content: ' {'; | |
| font-size: 1.2em; } | |
| cond::after { | |
| font-family: serif; | |
| color: black; | |
| font-style: normal; | |
| content: '} '; | |
| font-size: 1.2em; } | |
| /*# sourceMappingURL=axiomatic.css.map */ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| { | |
| "version": 3, | |
| "mappings": ";AAcA,KAAM;EACF,OAAO,EAAE,YAAY;EACrB,UAAU,EAAE,MAAM;EAClB,MAAM,EAAE,QAAQ;EAChB,SAAS,EAAE,IAAI;EACf,WAAM;IACF,MAAM,EAAE,MAAM;;AAGtB,IAAK;EACD,IAAI,EAAE,OAAO;EACb,KAAK,EAAE,OAAO;EACd,OAAO,EAAE,MAAM;;AAEnB,WAAY;EACR,OAAO,EAAE,GAAG;EACZ,UAAU,EAAE,MAAM;;AAEtB,UAAW;EACP,OAAO,EAAE,GAAG;EACZ,UAAU,EAAE,MAAM;;AAEtB,YAAa;EAnCT,WAAW,EAAE,sBAAsB;EACnC,UAAU,EAAE,MAAM;EAClB,KAAK,EAAE,KAAK;;AAoChB,YAAa;EAjCT,WAAW,EAAE,KAAK;EAClB,KAAK,EAAE,KAAK;EACZ,UAAU,EAAE,MAAM;EAiClB,OAAO,EAAE,KAAK;;AAElB,WAAY;EArCR,WAAW,EAAE,KAAK;EAClB,KAAK,EAAE,KAAK;EACZ,UAAU,EAAE,MAAM;EAqClB,OAAO,EAAE,GAAG;;AAEhB,eAAgB;EAzCZ,WAAW,EAAE,KAAK;EAClB,KAAK,EAAE,KAAK;EACZ,UAAU,EAAE,MAAM;EAyClB,OAAO,EAAE,KAAK;;AAElB,cAAe;EA7CX,WAAW,EAAE,KAAK;EAClB,KAAK,EAAE,KAAK;EACZ,UAAU,EAAE,MAAM;EA6ClB,OAAO,EAAE,GAAG;;AAEhB,kCAAmC;EAjD/B,WAAW,EAAE,KAAK;EAClB,KAAK,EAAE,KAAK;EACZ,UAAU,EAAE,MAAM;EAiDlB,OAAO,EAAE,IAAI;;AAEjB,MAAO;EArDH,WAAW,EAAE,KAAK;EAClB,KAAK,EAAE,KAAK;EACZ,UAAU,EAAE,MAAM;EAIlB,UAAU,EAAE,MAAM;EAiDlB,SAAS,EAAE,KAAK;;AAEpB,cAAe;EAzDX,WAAW,EAAE,KAAK;EAClB,KAAK,EAAE,KAAK;EACZ,UAAU,EAAE,MAAM;EAyDlB,OAAO,EAAE,IAAI;EACb,SAAS,EAAE,KAAK;;AAEpB,aAAc;EA9DV,WAAW,EAAE,KAAK;EAClB,KAAK,EAAE,KAAK;EACZ,UAAU,EAAE,MAAM;EA8DlB,OAAO,EAAE,GAAG;EACZ,SAAS,EAAE,KAAK;;AAEpB,4BAA6B;EACzB,OAAO,EAAE,KAAK;EACd,KAAK,EAAE,KAAK;;AAEhB,mCAAoC;EAvEhC,WAAW,EAAE,KAAK;EAClB,KAAK,EAAE,KAAK;EACZ,UAAU,EAAE,MAAM;EAuElB,OAAO,EAAE,MAAM;;AAEnB,UAAM;EAhFF,WAAW,EAAE,sBAAsB;EACnC,UAAU,EAAE,MAAM;EAClB,KAAK,EAAE,KAAK;EAgFZ,OAAO,EAAE,KAAK;EACd,OAAO,EAAE,GAAG;;AAEhB,GAAI;EAEA,UAAU,EAAE,eAAe;EAC3B,QAAQ,EAAE,QAAQ;EAClB,aAAa,EAAE,GAAG;;AAEtB,IAAK;EACD,QAAQ,EAAE,QAAQ;EAClB,KAAK,EAAE,CAAC;EACR,GAAG,EAAE,KAAK;EACV,KAAK,EAAE,KAAK;EACZ,WAAW,EAAE,SAAS;EACtB,SAAS,EAAE,KAAK;;AAEpB,OAAQ;EACJ,OAAO,EAAE,YAAY;EACrB,QAAQ,EAAE,QAAQ;EAClB,OAAO,EAAE,KAAK;EACd,SAAS,EAAE,KAAK;EAChB,cAAc,EAAE,MAAM;EAEtB,WAAI;IACA,OAAO,EAAE,SAAS;IAElB,eAAI;MACA,OAAO,EAAE,UAAU;MAEnB,2BAAc;QACV,aAAa,EAAE,GAAG;EAK9B,eAAU;IACN,OAAO,EAAE,KAAK;IACd,QAAQ,EAAE,QAAQ;IAClB,GAAG,EAAE,CAAC;IACN,IAAI,EAAE,CAAC;IACP,OAAO,EAAE,GAAG;IACZ,SAAS,EAAE,GAAG;IACd,UAAU,EAAE,MAAM;EAEtB,cAAS;IACL,OAAO,EAAE,KAAK;IACd,QAAQ,EAAE,QAAQ;IAClB,GAAG,EAAE,CAAC;IACN,KAAK,EAAE,CAAC;IACR,OAAO,EAAE,GAAG;IACZ,SAAS,EAAE,GAAG;IACd,UAAU,EAAE,MAAM;;AAG1B,IAAK;EApID,WAAW,EAAE,KAAK;EAClB,KAAK,EAAE,KAAK;EACZ,UAAU,EAAE,MAAM;EAIlB,UAAU,EAAE,MAAM;EAgIlB,OAAO,EAAE,MAAM;EAEf,YAAU;IAxIV,WAAW,EAAE,KAAK;IAClB,KAAK,EAAE,KAAK;IACZ,UAAU,EAAE,MAAM;IAwId,OAAO,EAAE,IAAI;IACb,SAAS,EAAE,KAAK;EAEpB,WAAS;IA7IT,WAAW,EAAE,KAAK;IAClB,KAAK,EAAE,KAAK;IACZ,UAAU,EAAE,MAAM;IA6Id,OAAO,EAAE,IAAI;IACb,SAAS,EAAE,KAAK", | |
| "sources": ["Axiomatic.css.scss"], | |
| "names": [], | |
| "file": "Axiomatic.css" | |
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| @mixin syntax { | |
| font-family: 'Fira Code', monospace; | |
| font-style: normal; | |
| color: green; | |
| } | |
| @mixin serif { | |
| font-family: serif; | |
| color: black; | |
| font-style: normal; | |
| } | |
| @mixin meta { | |
| @include serif; | |
| font-style: italic; | |
| } | |
| axiom { | |
| display: inline-block; | |
| text-align: center; | |
| margin: 1em 10px; | |
| font-size: 1rem; | |
| axiom { | |
| margin: 0 10px; | |
| } | |
| } | |
| text { | |
| font: initial; | |
| color: initial; | |
| display: inline; | |
| } | |
| and::before { | |
| content: '∧'; | |
| font-style: normal; | |
| } | |
| or::before { | |
| content: '∨'; | |
| font-style: normal; | |
| } | |
| syntax, aval { | |
| @include syntax; | |
| } | |
| aval::before { | |
| @include serif; | |
| content: "𝒜 ⟦"; | |
| } | |
| aval::after { | |
| @include serif; | |
| content: "⟧"; | |
| } | |
| listval::before { | |
| @include serif; | |
| content: "ℒ ⟦"; | |
| } | |
| listval::after { | |
| @include serif; | |
| content: "⟧"; | |
| } | |
| listval > :not(:last-child)::after { | |
| @include serif; | |
| content: ', '; | |
| } | |
| update { | |
| @include meta; | |
| font-size: 0.9em; | |
| } | |
| update::before { | |
| @include serif; | |
| content: ' ['; | |
| font-size: 1.1em; | |
| } | |
| update::after { | |
| @include serif; | |
| content: ']'; | |
| font-size: 1.1em; | |
| } | |
| update > :first-child::after { | |
| content: ' ↦ '; | |
| color: black; | |
| } | |
| update > listval:first-child::after { | |
| @include serif; | |
| content: '⟧ ↦ '; | |
| } | |
| given { | |
| @include syntax; | |
| display: block; | |
| padding: 5px; | |
| } | |
| stm { | |
| @extend given; | |
| border-top: 1px solid black; | |
| position: relative; | |
| padding-right: 2em; | |
| } | |
| rule { | |
| position: absolute; | |
| right: 0; | |
| top: 0.1em; | |
| color: black; | |
| font-family: monospace; | |
| font-size: 0.8em; | |
| } | |
| ternary { | |
| display: inline-table; | |
| position: relative; | |
| padding: 0 1em; | |
| font-size: 0.8em; | |
| vertical-align: middle; | |
| > * { | |
| display: table-row; | |
| > * { | |
| display: table-cell; | |
| &:first-child { | |
| padding-right: 1em; | |
| } | |
| } | |
| } | |
| &::before { | |
| display: block; | |
| position: absolute; | |
| top: 0; | |
| left: 0; | |
| content: '{'; | |
| font-size: 2em; | |
| font-style: normal; | |
| } | |
| &::after { | |
| display: block; | |
| position: absolute; | |
| top: 0; | |
| right: 0; | |
| content: '}'; | |
| font-size: 2em; | |
| font-style: normal; | |
| } | |
| } | |
| cond { | |
| @include meta; | |
| display: inline; | |
| &::before { | |
| @include serif; | |
| content: ' {'; | |
| font-size: 1.2em; | |
| } | |
| &::after { | |
| @include serif; | |
| content: '} '; | |
| font-size: 1.2em; | |
| } | |
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| <!DOCTYPE html> | |
| <html> | |
| <head> | |
| <link rel="stylesheet" href="axiomatic.css"> | |
| <title>Axiomatic semantic rules of the While language</title> | |
| </head> | |
| <body> | |
| <h1>Axiomatic semantic rules of the While language</h1> | |
| <cite>Charlie Harding</cite> | |
| <h2>Skip</h2> | |
| <axiom> | |
| <stm><rule>SKIP</rule><cond>P</cond>skip<cond>P</cond></stm> | |
| </axiom> | |
| <h2>Sequences</h2> | |
| <axiom> | |
| <axiom><given><cond>P</cond>S₁<cond>R</cond></given></axiom> | |
| <axiom><given><cond>R</cond>S₂<cond>Q</cond></given></axiom> | |
| <stm><rule>SEQ</rule><cond>P</cond>S₁ ; S₂<cond>Q</cond></stm> | |
| </axiom> | |
| <h2>Conditional</h2> | |
| <axiom> | |
| <axiom><given><cond>P <and/> b</cond>S₁<cond>Q</cond></given></axiom> | |
| <axiom><given><cond>P <and/> ~b</cond>S₂<cond>Q</cond></given></axiom> | |
| <stm><rule>COND</rule><cond>P</cond>if b then S₁ else S₂<cond>Q</cond></stm> | |
| </axiom> | |
| <h2>Loops</h2> | |
| <axiom> | |
| <axiom><given><cond>P <and/> b</cond>S<cond>P</cond></given></axiom> | |
| <stm><rule>LOOP</rule><cond>P</cond>while b do S<cond>P <and/> ~b</cond></stm> | |
| </axiom> | |
| <axiom> | |
| <axiom><given><cond>P <or/> (Q <and/> ~b)</cond>S<cond>Q</cond></given></axiom> | |
| <stm><rule>REPT</rule><cond>P</cond>repeat S until b<cond>Q <and/> b</cond></stm> | |
| </axiom> | |
| <h2>Assignment</h2> | |
| <axiom> | |
| <stm><rule>ASSN</rule><cond>P<update><syntax>x</syntax><aval>a</aval></update></cond>x := a<cond>P</cond></stm> | |
| </axiom> | |
| <!-- <axiom> | |
| <stm> | |
| <rule>ARRA</rule> | |
| <cond>P<update><syntax>a₁</syntax><syntax>a₁<update><syntax>a₂</syntax><syntax>x</syntax></update></syntax></update></cond> | |
| a₁[a₂] := x | |
| <cond>P</cond></stm> | |
| </axiom> | |
| <axiom> | |
| <stm> | |
| <rule>ARRA</rule> | |
| <cond>P<update><syntax>a₁[a₂]</syntax><syntax>x</syntax></update></cond> | |
| a₁[a₂] := x | |
| <cond>P</cond> | |
| </stm> | |
| </axiom> | |
| <h3>Example</h3> | |
| <code> | |
| varName :: LValue -> State -> String | |
| varName (Var var) s = var | |
| varName (Array arr i) s = case a_syntax i s of | |
| 0 -> arr | |
| i_syntax -> arr ++ ";" ++ i_syntax | |
| s_ds (Assign var x) s = update (varName var s) a_syntax x s | |
| </code> | |
| <axiom> | |
| <axiom> | |
| <axiom> | |
| <stm><cond>(<syntax>x</syntax> = 5)<update><syntax>x</syntax><syntax>(y = 12) ? 5 : 7</syntax></update></cond>x := (y = 12 ? 5 : 7)<cond><syntax>x</syntax> = 5</cond></stm> | |
| </axiom> | |
| <stm><cond><syntax>(y = 12 ? 5 : 7)</syntax> = 5</cond>x := (y = 12 ? 5 : 7)<cond><syntax>x</syntax> = 5</cond></stm> | |
| </axiom> | |
| <stm><cond><syntax>y</syntax> = 12</cond>x := (y = 12 ? 5 : 7)<cond><syntax>x</syntax> = 5</cond></stm> | |
| </axiom> --> | |
| </body> | |
| </html> |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment