-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
1 lines (1 loc) · 98.1 KB
/
index.html
1
<html><head><meta content="text/html; charset=UTF-8" http-equiv="content-type"><style type="text/css">ul.lst-kix_82er1brroaog-8{list-style-type:none}ul.lst-kix_82er1brroaog-7{list-style-type:none}ul.lst-kix_82er1brroaog-2{list-style-type:none}ul.lst-kix_82er1brroaog-0{list-style-type:none}ul.lst-kix_82er1brroaog-6{list-style-type:none}ul.lst-kix_82er1brroaog-5{list-style-type:none}ul.lst-kix_82er1brroaog-4{list-style-type:none}ul.lst-kix_82er1brroaog-3{list-style-type:none}.lst-kix_36o98skmki7a-1>li:before{content:"\0025cb "}.lst-kix_36o98skmki7a-0>li:before{content:"\0025cf "}.lst-kix_36o98skmki7a-2>li:before{content:"\0025a0 "}ul.lst-kix_36o98skmki7a-0{list-style-type:none}.lst-kix_36o98skmki7a-5>li:before{content:"\0025a0 "}.lst-kix_bwcnx74ykyp6-5>li:before{content:"\0025a0 "}ul.lst-kix_36o98skmki7a-2{list-style-type:none}.lst-kix_36o98skmki7a-4>li:before{content:"\0025cb "}.lst-kix_36o98skmki7a-6>li:before{content:"\0025cf "}ul.lst-kix_36o98skmki7a-1{list-style-type:none}.lst-kix_36o98skmki7a-3>li:before{content:"\0025cf "}ul.lst-kix_36o98skmki7a-4{list-style-type:none}.lst-kix_36o98skmki7a-7>li:before{content:"\0025cb "}ul.lst-kix_36o98skmki7a-3{list-style-type:none}ul.lst-kix_36o98skmki7a-6{list-style-type:none}.lst-kix_bwcnx74ykyp6-4>li:before{content:"\0025cb "}.lst-kix_bwcnx74ykyp6-8>li:before{content:"\0025a0 "}ul.lst-kix_36o98skmki7a-5{list-style-type:none}ul.lst-kix_36o98skmki7a-8{list-style-type:none}.lst-kix_bwcnx74ykyp6-1>li:before{content:"\0025cb "}ul.lst-kix_36o98skmki7a-7{list-style-type:none}.lst-kix_bwcnx74ykyp6-3>li:before{content:"\0025cf "}.lst-kix_bwcnx74ykyp6-2>li:before{content:"\0025a0 "}.lst-kix_82er1brroaog-1>li{counter-increment:lst-ctn-kix_82er1brroaog-1}.lst-kix_36o98skmki7a-8>li:before{content:"\0025a0 "}.lst-kix_bwcnx74ykyp6-7>li:before{content:"\0025cb "}.lst-kix_bwcnx74ykyp6-6>li:before{content:"\0025cf "}.lst-kix_pqyspzcpl1nw-3>li:before{content:"\0025cf "}.lst-kix_pqyspzcpl1nw-2>li:before{content:"\0025a0 "}.lst-kix_pqyspzcpl1nw-4>li:before{content:"\0025cb "}.lst-kix_pqyspzcpl1nw-7>li:before{content:"\0025cb "}.lst-kix_pqyspzcpl1nw-6>li:before{content:"\0025cf "}.lst-kix_pqyspzcpl1nw-5>li:before{content:"\0025a0 "}ul.lst-kix_l5ek6igvtcm9-7{list-style-type:none}ul.lst-kix_l5ek6igvtcm9-8{list-style-type:none}ul.lst-kix_l5ek6igvtcm9-5{list-style-type:none}ul.lst-kix_l5ek6igvtcm9-6{list-style-type:none}ul.lst-kix_l5ek6igvtcm9-3{list-style-type:none}ul.lst-kix_l5ek6igvtcm9-4{list-style-type:none}ul.lst-kix_l5ek6igvtcm9-1{list-style-type:none}ul.lst-kix_l5ek6igvtcm9-2{list-style-type:none}ul.lst-kix_l5ek6igvtcm9-0{list-style-type:none}.lst-kix_bwcnx74ykyp6-0>li:before{content:"\0025cf "}.lst-kix_pqyspzcpl1nw-0>li:before{content:"\0025cf "}.lst-kix_pqyspzcpl1nw-1>li:before{content:"\0025cb "}.lst-kix_dg4znuy70dl9-5>li:before{content:"\0025a0 "}.lst-kix_dg4znuy70dl9-7>li:before{content:"\0025cb "}.lst-kix_pqyspzcpl1nw-8>li:before{content:"\0025a0 "}.lst-kix_kt1x3xteemmb-8>li:before{content:"\0025a0 "}.lst-kix_5qumemskpxo9-0>li:before{content:"\0025cf "}.lst-kix_kt1x3xteemmb-6>li:before{content:"\0025cf "}.lst-kix_kt1x3xteemmb-0>li:before{content:"\0025cf "}ul.lst-kix_bwcnx74ykyp6-3{list-style-type:none}ul.lst-kix_bwcnx74ykyp6-4{list-style-type:none}ul.lst-kix_bwcnx74ykyp6-1{list-style-type:none}ul.lst-kix_bwcnx74ykyp6-2{list-style-type:none}ul.lst-kix_bwcnx74ykyp6-7{list-style-type:none}ul.lst-kix_bwcnx74ykyp6-8{list-style-type:none}ul.lst-kix_bwcnx74ykyp6-5{list-style-type:none}ul.lst-kix_bwcnx74ykyp6-6{list-style-type:none}.lst-kix_kt1x3xteemmb-4>li:before{content:"\0025cb "}.lst-kix_dg4znuy70dl9-1>li:before{content:"\0025cb "}.lst-kix_kt1x3xteemmb-2>li:before{content:"\0025a0 "}.lst-kix_dg4znuy70dl9-3>li:before{content:"\0025cf "}ul.lst-kix_bwcnx74ykyp6-0{list-style-type:none}.lst-kix_l5ek6igvtcm9-0>li:before{content:"\0025cf "}.lst-kix_5qumemskpxo9-8>li:before{content:"\0025a0 "}.lst-kix_l5ek6igvtcm9-4>li:before{content:"\0025cb "}ul.lst-kix_pqyspzcpl1nw-1{list-style-type:none}ul.lst-kix_pqyspzcpl1nw-2{list-style-type:none}.lst-kix_5qumemskpxo9-4>li:before{content:"\0025cb "}.lst-kix_5qumemskpxo9-6>li:before{content:"\0025cf "}ul.lst-kix_pqyspzcpl1nw-3{list-style-type:none}.lst-kix_l5ek6igvtcm9-6>li:before{content:"\0025cf "}ul.lst-kix_pqyspzcpl1nw-4{list-style-type:none}.lst-kix_l5ek6igvtcm9-8>li:before{content:"\0025a0 "}ul.lst-kix_pqyspzcpl1nw-5{list-style-type:none}ul.lst-kix_pqyspzcpl1nw-6{list-style-type:none}ul.lst-kix_pqyspzcpl1nw-7{list-style-type:none}ul.lst-kix_pqyspzcpl1nw-8{list-style-type:none}.lst-kix_5qumemskpxo9-2>li:before{content:"\0025a0 "}.lst-kix_l5ek6igvtcm9-2>li:before{content:"\0025a0 "}.lst-kix_o50dswdx9e7q-7>li:before{content:"\0025cb "}.lst-kix_o50dswdx9e7q-6>li:before{content:"\0025cf "}.lst-kix_ooiavzuaqt14-2>li:before{content:"\0025a0 "}.lst-kix_o50dswdx9e7q-5>li:before{content:"\0025a0 "}.lst-kix_ooiavzuaqt14-3>li:before{content:"\0025cf "}.lst-kix_ooiavzuaqt14-4>li:before{content:"\0025cb "}.lst-kix_o50dswdx9e7q-4>li:before{content:"\0025cb "}.lst-kix_ooiavzuaqt14-6>li:before{content:"\0025cf "}.lst-kix_ooiavzuaqt14-5>li:before{content:"\0025a0 "}.lst-kix_ooiavzuaqt14-7>li:before{content:"\0025cb "}ol.lst-kix_82er1brroaog-1{list-style-type:none}.lst-kix_ooiavzuaqt14-8>li:before{content:"\0025a0 "}.lst-kix_o50dswdx9e7q-8>li:before{content:"\0025a0 "}ul.lst-kix_kt1x3xteemmb-4{list-style-type:none}ul.lst-kix_kt1x3xteemmb-5{list-style-type:none}.lst-kix_82er1brroaog-5>li:before{content:"\0025a0 "}.lst-kix_82er1brroaog-6>li:before{content:"\0025cf "}ul.lst-kix_kt1x3xteemmb-2{list-style-type:none}ul.lst-kix_kt1x3xteemmb-3{list-style-type:none}ul.lst-kix_kt1x3xteemmb-0{list-style-type:none}ul.lst-kix_kt1x3xteemmb-1{list-style-type:none}.lst-kix_82er1brroaog-3>li:before{content:"\0025cf "}.lst-kix_82er1brroaog-4>li:before{content:"\0025cb "}.lst-kix_82er1brroaog-7>li:before{content:"\0025cb "}.lst-kix_82er1brroaog-8>li:before{content:"\0025a0 "}.lst-kix_a83zt6unfz9-8>li:before{content:"\0025a0 "}.lst-kix_a83zt6unfz9-7>li:before{content:"\0025cb "}ul.lst-kix_kt1x3xteemmb-8{list-style-type:none}.lst-kix_a83zt6unfz9-6>li:before{content:"\0025cf "}ul.lst-kix_kt1x3xteemmb-6{list-style-type:none}ul.lst-kix_kt1x3xteemmb-7{list-style-type:none}ul.lst-kix_pqyspzcpl1nw-0{list-style-type:none}.lst-kix_a83zt6unfz9-3>li:before{content:"\0025cf "}.lst-kix_o50dswdx9e7q-1>li:before{content:"\0025cb "}.lst-kix_a83zt6unfz9-1>li:before{content:"\0025cb "}.lst-kix_a83zt6unfz9-5>li:before{content:"\0025a0 "}.lst-kix_o50dswdx9e7q-3>li:before{content:"\0025cf "}.lst-kix_82er1brroaog-0>li:before{content:"\0025cf "}.lst-kix_a83zt6unfz9-0>li:before{content:"\0025cf "}.lst-kix_a83zt6unfz9-4>li:before{content:"\0025cb "}.lst-kix_o50dswdx9e7q-2>li:before{content:"\0025a0 "}.lst-kix_82er1brroaog-1>li:before{content:"" counter(lst-ctn-kix_82er1brroaog-1,lower-latin) ". "}.lst-kix_82er1brroaog-2>li:before{content:"\0025a0 "}.lst-kix_a83zt6unfz9-2>li:before{content:"\0025a0 "}.lst-kix_o50dswdx9e7q-0>li:before{content:"\0025cf "}.lst-kix_f7xmydnxl64-2>li:before{content:"\0025a0 "}.lst-kix_f7xmydnxl64-4>li:before{content:"\0025cb "}.lst-kix_f7xmydnxl64-3>li:before{content:"\0025cf "}.lst-kix_f7xmydnxl64-7>li:before{content:"\0025cb "}.lst-kix_f7xmydnxl64-0>li:before{content:"\0025cf "}.lst-kix_f7xmydnxl64-8>li:before{content:"\0025a0 "}.lst-kix_f7xmydnxl64-1>li:before{content:"\0025cb "}.lst-kix_ooiavzuaqt14-1>li:before{content:"\0025cb "}.lst-kix_f7xmydnxl64-6>li:before{content:"\0025cf "}.lst-kix_ooiavzuaqt14-0>li:before{content:"\0025cf "}.lst-kix_f7xmydnxl64-5>li:before{content:"\0025a0 "}ul.lst-kix_f7xmydnxl64-8{list-style-type:none}.lst-kix_dg4znuy70dl9-4>li:before{content:"\0025cb "}ul.lst-kix_f7xmydnxl64-6{list-style-type:none}ul.lst-kix_f7xmydnxl64-7{list-style-type:none}ul.lst-kix_f7xmydnxl64-4{list-style-type:none}ul.lst-kix_f7xmydnxl64-5{list-style-type:none}ul.lst-kix_f7xmydnxl64-2{list-style-type:none}ul.lst-kix_f7xmydnxl64-3{list-style-type:none}ul.lst-kix_f7xmydnxl64-0{list-style-type:none}ul.lst-kix_f7xmydnxl64-1{list-style-type:none}.lst-kix_dg4znuy70dl9-0>li:before{content:"\0025cf "}.lst-kix_dg4znuy70dl9-8>li:before{content:"\0025a0 "}.lst-kix_dg4znuy70dl9-6>li:before{content:"\0025cf "}ul.lst-kix_o50dswdx9e7q-5{list-style-type:none}ul.lst-kix_o50dswdx9e7q-6{list-style-type:none}ul.lst-kix_o50dswdx9e7q-7{list-style-type:none}ul.lst-kix_o50dswdx9e7q-8{list-style-type:none}ul.lst-kix_o50dswdx9e7q-1{list-style-type:none}ul.lst-kix_o50dswdx9e7q-2{list-style-type:none}ul.lst-kix_o50dswdx9e7q-3{list-style-type:none}ul.lst-kix_o50dswdx9e7q-4{list-style-type:none}ul.lst-kix_o50dswdx9e7q-0{list-style-type:none}.lst-kix_kt1x3xteemmb-7>li:before{content:"\0025cb "}.lst-kix_5qumemskpxo9-1>li:before{content:"\0025cb "}.lst-kix_kt1x3xteemmb-5>li:before{content:"\0025a0 "}ul.lst-kix_5qumemskpxo9-8{list-style-type:none}ul.lst-kix_5qumemskpxo9-7{list-style-type:none}.lst-kix_kt1x3xteemmb-1>li:before{content:"\0025cb "}ul.lst-kix_5qumemskpxo9-4{list-style-type:none}ul.lst-kix_5qumemskpxo9-3{list-style-type:none}ul.lst-kix_5qumemskpxo9-6{list-style-type:none}ul.lst-kix_5qumemskpxo9-5{list-style-type:none}ul.lst-kix_5qumemskpxo9-0{list-style-type:none}ul.lst-kix_5qumemskpxo9-2{list-style-type:none}.lst-kix_kt1x3xteemmb-3>li:before{content:"\0025cf "}ul.lst-kix_5qumemskpxo9-1{list-style-type:none}ol.lst-kix_82er1brroaog-1.start{counter-reset:lst-ctn-kix_82er1brroaog-1 0}.lst-kix_dg4znuy70dl9-2>li:before{content:"\0025a0 "}ul.lst-kix_ooiavzuaqt14-0{list-style-type:none}ul.lst-kix_ooiavzuaqt14-2{list-style-type:none}ul.lst-kix_ooiavzuaqt14-1{list-style-type:none}.lst-kix_5qumemskpxo9-7>li:before{content:"\0025cb "}ul.lst-kix_dg4znuy70dl9-1{list-style-type:none}.lst-kix_l5ek6igvtcm9-5>li:before{content:"\0025a0 "}ul.lst-kix_dg4znuy70dl9-0{list-style-type:none}.lst-kix_5qumemskpxo9-5>li:before{content:"\0025a0 "}ul.lst-kix_dg4znuy70dl9-5{list-style-type:none}ul.lst-kix_dg4znuy70dl9-4{list-style-type:none}ul.lst-kix_dg4znuy70dl9-3{list-style-type:none}ul.lst-kix_dg4znuy70dl9-2{list-style-type:none}ul.lst-kix_dg4znuy70dl9-8{list-style-type:none}ul.lst-kix_dg4znuy70dl9-7{list-style-type:none}ul.lst-kix_dg4znuy70dl9-6{list-style-type:none}.lst-kix_l5ek6igvtcm9-7>li:before{content:"\0025cb "}ul.lst-kix_ooiavzuaqt14-4{list-style-type:none}ul.lst-kix_ooiavzuaqt14-3{list-style-type:none}ul.lst-kix_ooiavzuaqt14-6{list-style-type:none}ul.lst-kix_ooiavzuaqt14-5{list-style-type:none}.lst-kix_5qumemskpxo9-3>li:before{content:"\0025cf "}ul.lst-kix_ooiavzuaqt14-8{list-style-type:none}ul.lst-kix_ooiavzuaqt14-7{list-style-type:none}ul.lst-kix_a83zt6unfz9-0{list-style-type:none}ul.lst-kix_a83zt6unfz9-1{list-style-type:none}ul.lst-kix_a83zt6unfz9-2{list-style-type:none}ul.lst-kix_a83zt6unfz9-3{list-style-type:none}ul.lst-kix_a83zt6unfz9-4{list-style-type:none}ul.lst-kix_a83zt6unfz9-5{list-style-type:none}ul.lst-kix_a83zt6unfz9-6{list-style-type:none}ul.lst-kix_a83zt6unfz9-7{list-style-type:none}ul.lst-kix_a83zt6unfz9-8{list-style-type:none}li.li-bullet-0:before{margin-left:-18pt;white-space:nowrap;display:inline-block;min-width:18pt}.lst-kix_l5ek6igvtcm9-3>li:before{content:"\0025cf "}.lst-kix_l5ek6igvtcm9-1>li:before{content:"\0025cb "}ol{margin:0;padding:0}table td,table th{padding:0}.c25{margin-left:17pt;padding-top:0pt;padding-bottom:0pt;line-height:1.35;orphans:2;widows:2;text-align:right;margin-right:4pt}.c6{margin-left:36pt;padding-top:0pt;padding-left:0pt;padding-bottom:0pt;line-height:1.15;orphans:2;widows:2;text-align:left}.c15{color:#434343;font-weight:400;text-decoration:none;vertical-align:baseline;font-size:14pt;font-family:"Times New Roman";font-style:normal}.c1{color:#000000;font-weight:700;text-decoration:none;vertical-align:baseline;font-size:26pt;font-family:"Times New Roman";font-style:normal}.c8{padding-top:18pt;padding-bottom:6pt;line-height:1.15;page-break-after:avoid;orphans:2;widows:2;text-align:left}.c5{padding-top:0pt;padding-bottom:0pt;line-height:1.15;orphans:2;widows:2;text-align:left;height:12pt}.c22{color:#000000;font-weight:400;text-decoration:none;vertical-align:baseline;font-size:16pt;font-family:"Times New Roman";font-style:normal}.c32{padding-top:0pt;padding-bottom:3pt;line-height:1.15;page-break-after:avoid;orphans:2;widows:2;text-align:left}.c10{color:#666666;font-weight:400;text-decoration:none;vertical-align:baseline;font-size:12pt;font-family:"Times New Roman";font-style:normal}.c2{padding-top:20pt;padding-bottom:6pt;line-height:1.15;page-break-after:avoid;orphans:2;widows:2;text-align:left}.c0{color:#000000;font-weight:400;text-decoration:none;vertical-align:baseline;font-size:12pt;font-family:"Times New Roman";font-style:normal}.c19{padding-top:16pt;padding-bottom:4pt;line-height:1.15;page-break-after:avoid;orphans:2;widows:2;text-align:left}.c14{color:#000000;font-weight:400;text-decoration:none;vertical-align:baseline;font-size:20pt;font-family:"Times New Roman";font-style:normal}.c21{padding-top:14pt;padding-bottom:4pt;line-height:1.15;page-break-after:avoid;orphans:2;widows:2;text-align:left}.c31{color:#000000;text-decoration:none;vertical-align:baseline;font-size:12pt;font-family:"Times New Roman";font-style:normal}.c27{padding-top:0pt;padding-bottom:0pt;line-height:1.35;orphans:2;widows:2;text-align:left}.c33{font-weight:400;text-decoration:none;vertical-align:baseline;font-size:12pt;font-family:"Times New Roman";font-style:normal}.c7{padding-top:0pt;padding-bottom:0pt;line-height:1.15;orphans:2;widows:2;text-align:left}.c34{color:#000000;text-decoration:none;vertical-align:baseline;font-size:12pt}.c16{text-decoration-skip-ink:none;-webkit-text-decoration-skip:none;color:#1155cc;text-decoration:underline}.c30{background-color:#ffffff;max-width:468pt;padding:72pt 72pt 72pt 72pt}.c20{text-decoration-skip-ink:none;-webkit-text-decoration-skip:none;text-decoration:underline}.c18{color:inherit;text-decoration:inherit}.c3{padding:0;margin:0}.c28{margin-left:17pt;margin-right:4pt}.c11{margin-left:72pt;padding-left:0pt}.c13{margin-left:108pt;padding-left:0pt}.c17{background-color:#ffffff;color:#222222}.c23{font-weight:400;font-family:"Courier New"}.c26{color:#9900ff}.c12{text-indent:36pt}.c4{font-weight:700}.c24{height:14pt}.c29{color:#ff00ff}.c9{font-style:italic}.title{padding-top:0pt;color:#000000;font-weight:700;font-size:26pt;padding-bottom:3pt;font-family:"Times New Roman";line-height:1.15;page-break-after:avoid;orphans:2;widows:2;text-align:left}.subtitle{padding-top:0pt;color:#666666;font-size:15pt;padding-bottom:16pt;font-family:"Times New Roman";line-height:1.15;page-break-after:avoid;orphans:2;widows:2;text-align:left}li{color:#000000;font-size:12pt;font-family:"Times New Roman"}p{margin:0;color:#000000;font-size:12pt;font-family:"Times New Roman"}h1{padding-top:20pt;color:#000000;font-size:20pt;padding-bottom:6pt;font-family:"Times New Roman";line-height:1.15;page-break-after:avoid;orphans:2;widows:2;text-align:left}h2{padding-top:18pt;color:#000000;font-size:16pt;padding-bottom:6pt;font-family:"Times New Roman";line-height:1.15;page-break-after:avoid;orphans:2;widows:2;text-align:left}h3{padding-top:16pt;color:#434343;font-size:14pt;padding-bottom:4pt;font-family:"Times New Roman";line-height:1.15;page-break-after:avoid;orphans:2;widows:2;text-align:left}h4{padding-top:14pt;color:#666666;font-size:12pt;padding-bottom:4pt;font-family:"Times New Roman";line-height:1.15;page-break-after:avoid;orphans:2;widows:2;text-align:left}h5{padding-top:12pt;color:#666666;font-size:11pt;padding-bottom:4pt;font-family:"Times New Roman";line-height:1.15;page-break-after:avoid;orphans:2;widows:2;text-align:left}h6{padding-top:12pt;color:#666666;font-size:11pt;padding-bottom:4pt;font-family:"Times New Roman";line-height:1.15;page-break-after:avoid;font-style:italic;orphans:2;widows:2;text-align:left}</style></head><body class="c30 doc-content"><p class="c32 title" id="h.4s1szosqa07r"><span class="c1">Final Portfolio</span></p><h1 class="c2" id="h.f22086a0meip"><span class="c14">Draft Research Questions</span></h1><p class="c7"><span class="c0">From oldest to newest:</span></p><ul class="c3 lst-kix_a83zt6unfz9-0 start"><li class="c6 li-bullet-0"><span>For computer scientists and mathematicians, there has always been a thick wall between the specification of programs in natural language and the implementation of them in mathematical syntax or computer code; this wall enables errors, security issues, and divergences in implementation through mistranslation. </span><span class="c4">How can the semantics of restricted natural language be used to both design </span><span class="c4 c9">and</span><span class="c4 c31"> implement automata, so that program specifications can act as a single source of truth?</span></li><li class="c6 li-bullet-0"><span class="c0">How can restricted, prescriptive grammar be used to write specifications that are both human and machine-readable?</span></li><li class="c6 li-bullet-0"><span class="c0">How can natural language be formalized to make the process of writing specifications for complex software easier?</span></li></ul><h1 class="c2" id="h.mt5tkvr4e16o"><span class="c14">Draft Claim</span></h1><p class="c7"><span class="c0">As cool as computer science is, it is not a one-on-one conversation with the machine. It’s a collaborative process that for the most part takes place outside the text editor. When dozens of people are all working towards the development of a single product, all of them sharing different literacy in computer programming and user design, they need a guiding force. That is the purpose of the specification. However, specifications can be hard to understand, and even lead to bugs and implementation differences, the things they’re meant to avoid. Natural language specifications can be challenging to write clearly, and formal specifications, usually relying on mathematical syntax, can be challenging to parse for the uninitiated.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">In this presentation, I aim to show that the benefits of both informal natural language specifications and formal mathematical specifications can be combined with minimal downsides, while at the same time allowing said specifications to be read by both humans and computers. By writing in this ideal specification language, engineers can write specifications that can be read and verified by anyone with the appropriate domain knowledge and turned into an executable program, creating a single source of truth for an application. This can be accomplished through extremely restricted prescriptive grammar. Through this, specifications can be easily parsed by computers and humans can avoid ambiguity when interpreting them.</span></p><h1 class="c2" id="h.r4f0iw6bnx1x"><span class="c14">Abstract</span></h1><p class="c7 c12"><span>Specifications, documents explicitly and intricately defining the behavior of a piece of software, are commonly used in the information technology industry to help large teams design and iterate on complex systems. There are, traditionally, two kinds of specifications. Natural-language specifications are easy to read and write, but very challenging to write well, and their lack of formality due to over-expressiveness creates misunderstandings that lead to grave errors in implementation. Formal specifications lean on propositional logic and set theory from mathematics to construct rigorous specifications, but can be hard to read for those without advanced knowledge in discrete math and computer science. Computer scientists strictly believe that natural language is by definition informal, making it unfit for writing specifications, but natural language is still </span><span class="c9">heavily</span><span class="c4"> </span><span class="c0">used over formal specifications to describe complex systems. This presentation explores a possible marriage of these opposing approaches—a formal specification language that uses a prescriptive subset of the English language—through a toy specification language that can be parsed and error-checked by a computer program. By formalizing natural language in specifications, the barrier to describing and understanding mission-critical software can be significantly lowered.</span></p><h1 class="c2" id="h.vdr9biegz37o"><span class="c14">Acknowledgments</span></h1><p class="c7"><span class="c0">I am glad to acknowledge:</span></p><ul class="c3 lst-kix_f7xmydnxl64-0 start"><li class="c6 li-bullet-0"><span class="c0">Ms. Gardiner and Ms. Loi, for overlooking my research,</span></li><li class="c6 li-bullet-0"><span class="c0">the Computer Science and Information Sciences faculty, for supporting my CS journey at Poly, especially Ms. Guynn, Mr. Klett, and Mr. Polizano, who looked over parts of my presentation, and</span></li><li class="c6 li-bullet-0"><span class="c0">Mr. Nowakoski for igniting my passion for linguistics and being a guiding force early on in my capstone.</span></li></ul><h1 class="c2" id="h.cihj128riluk"><span class="c14">Bibliography</span></h1><p class="c25"><span class="c0">[1]</span></p><p class="c27 c28"><span class="c0">S. Bradner, “Key words for use in RFCs to Indicate Requirement Levels,” 1997. [Online]. Available: https://www.rfc-editor.org/rfc/rfc2119</span></p><p class="c25"><span class="c0">[2]</span></p><p class="c27 c28"><span>C.-C. Chiang, “TUG: An Executable Specification Language,” in </span><span class="c9">5th IEEE/ACIS International Conference on Computer and Information Science and 1st IEEE/ACIS International Workshop on Component-Based Software Engineering,Software Architecture and Reuse (ICIS-COMSAR’06)</span><span class="c0">, 2006, pp. 180–186. doi: 10.1109/ICIS-COMSAR.2006.85.</span></p><p class="c25"><span class="c0">[3]</span></p><p class="c27 c28"><span>N. E. Fuchs, “Specifications are (preferably) executable,” </span><span class="c9">Software engineering journal</span><span class="c0">, vol. 7, no. 5, pp. 323–334, 1992.</span></p><p class="c25"><span class="c0">[4]</span></p><p class="c27 c28"><span>I. J. Hayes and C. B. Jones, “Specifications are not (necessarily) executable,” </span><span class="c9">Software Engineering Journal</span><span class="c0">, vol. 4, no. 6, pp. 330–339, 1989.</span></p><p class="c25"><span class="c0">[5]</span></p><p class="c27 c28"><span class="c0">A. van Kesteren and D. Denicola, “Infra Standard,” Apr. 05, 2023. https://infra.spec.whatwg.org/</span></p><p class="c25"><span class="c0">[6]</span></p><p class="c27 c28"><span>H. U. Khan, I. Asghar, S. A. A. Ghayyur, and M. Raza, “An empirical study of software requirements verification and validation techniques along their mitigation strategies,” </span><span class="c9">Asian Journal of Computer and Information Systems</span><span class="c0">, vol. 3, no. 3, 2015, [Online]. Available: https://www.researchgate.net/profile/Ikram-Asghar/publication/281645652_An_Empirical_Study_of_Software_Requirements_Verification_and_Validation_Techniques_along_their_Mitigation_Strategies/links/55f2a17008ae199d47c4841c/An-Empirical-Study-of-Software-Requirements-Verification-and-Validation-Techniques-along-their-Mitigation-Strategies.pdf</span></p><p class="c25"><span class="c0">[7]</span></p><p class="c27 c28"><span>B. Meyer, “On formalism in specifications,” </span><span class="c9">IEEE software</span><span>, vol. 2, no. 1, p. 6, 1985.</span></p><h1 class="c2" id="h.7iu46tq820fc"><span class="c14">Review of Sources</span></h1><p class="c27"><span>H. U. Khan, I. Asghar, S. A. A. Ghayyur, and M. Raza, “An empirical study of software requirements verification and validation techniques along their mitigation strategies,” </span><span class="c9">Asian Journal of Computer and Information Systems</span><span class="c0">, vol. 3, no. 3, 2015, [Online]. Available: https://www.researchgate.net/profile/Ikram-Asghar/publication/281645652_An_Empirical_Study_of_Software_Requirements_Verification_and_Validation_Techniques_along_their_Mitigation_Strategies/links/55f2a17008ae199d47c4841c/An-Empirical-Study-of-Software-Requirements-Verification-and-Validation-Techniques-along-their-Mitigation-Strategies.pdf</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c4">DISTILLATION</span><span>: The article is composed of three sections: a literature review of </span><span class="c9">requirements verification</span><span> papers, a description of various verification techniques, and a survey of Pakistani software engineers on their frustrations with requirements engineering and how verification helps to resolve them. The authors believe that </span><span class="c9">requirements engineering</span><span> (RE)—a form of software engineering where a piece of software is explicitly designed before its production—is a crucial part of software development. An important part of the RE process is </span><span class="c9">verification and validation</span><span> (V&V), where engineers make sure that the software they’re writing follows the specification they’re implementing and is being written in an orderly manner. They found that there are six common techniques engineers use throughout V&V: </span><span class="c9">tracing</span><span> (justifying the specification), </span><span class="c9">prototyping</span><span>, </span><span class="c9">requirements testing</span><span>, </span><span class="c9">user manual writing</span><span>, </span><span class="c9">formal specification validation</span><span>, and </span><span class="c9">inspection</span><span class="c0">. From their survey of 55 experts from all walks of life in the Pakistani software industry, they found that the greatest challenges with implementing specifications were ambiguous requirements and, to a lesser extent, inconsistency and incomplete specifications, and the best tools to resolve them were implementation inspections and prototyping.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c4">CRITIQUE</span><span class="c0">: This article helped me to better concrete my research question alongside justifying many of my concerns surrounding my idea of “written specifications as code.” It introduced me to the term requirements engineering, which made it much easier for me to find literature related to my area of research. It also confirmed one of my suspicions about requirements engineering: translating a spec to a functional piece of software is fraught with ambiguity and inconsistency, to the point that many systems must be constructed around RE in order for it to go smoothly. I believe that many of these issues would be resolved by a subset of grammatical and semantic English that translates to computer code. Because of a limited subset of words and senses, it would be nigh impossible for there to be any semantic ambiguity in a specification. Because the specification can be translated to code, we can take advantage of existing tooling like linters to eliminate inconsistency. Having an executable specification also makes various V&V techniques irrelevant: the specification is the prototype and tests can be included in the specification as examples. An executable specification, therefore, allows humans to focus solely on writing a clear, error-free specification instead of having to juggle that with making an implementation. Now that I was sure that an answer to my research question would be valuable to the CS community, I used the article as a jumping-off point to explore how humans write specifications in various industries.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">S. Bradner, “Key words for use in RFCs to Indicate Requirement Levels,” 1997. [Online]. Available: https://www.rfc-editor.org/rfc/rfc2119</span></p><p class="c7"><span class="c0">B. Leiba, “Ambiguity of Uppercase vs Lowercase in RFC 2119 Key Words,” 2017. [Online]. Available: https://www.rfc-editor.org/rfc/rfc8174</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c4">DISTILLATION</span><span>: These two reports discuss the redefining of a group of keywords to indicate how urgently parts of a specification must be implemented. Request for Comments (RFC) 2119 creates these keywords, a mix of UPPERCASE verbs and adjectives such as </span><span class="c4">MUST</span><span> and </span><span class="c4">RECOMMENDED</span><span class="c0">, and assigns them specific meanings ranging from “you must implement this in order for your implementation to be valid” to “feel free to do or not to do this.” It also gives a phrase specification authors should use in their documents to indicate the redefining of these keywords, and some advice surrounding when using these keywords is appropriate. 2119 was created in reaction to many RFCs using keywords like these but no standard definition for them. RFC 8174 extends 2119, fixing an ambiguity issue with 2119: the casing of keywords. While 2119 shares the keywords as UPPERCASE, specification authors making use of 2119 would make use of both upper-and-lowercase words, causing readers to be confused about if they should interpret “must” as normal English or according to 2119. 8174 resolves this by clarifying that only UPPERCASE words hold the meaning defined in 2119, and gives specification authors a new phrase to use in their documents.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c4">CRITIQUE</span><span>: I believe these articles capture perfectly the intentions of my capstone project. They both demonstrate how we can use prescribed grammar to help computers understand natural language and how the lack of a prescribed grammar can cause ambiguity issues. Because 8174 requires that both words be UPPERCASE in order to have their prescribed meaning, computers can parse out the defined keywords and apply their meaning. Normal usage of these keywords is still preserved, as well, enabling machine-readable language and human-readable language in the same document. The extension of 2119 by 8174 demonstrates how important it is to be clear in the communication of a specification to avoid ambiguity, which I believe my question can solve by putting more emphasis on specifications. I do have some qualms. I do not like the mix of verbs and adjectives as keywords nor the substitute terms (one can substitute </span><span class="c4">MUST</span><span> for </span><span class="c4">REQUIRED</span><span> or </span><span class="c4">SHALL</span><span class="c0">), as I believe there should be one way to declare something. As much as I do like the ability to switch between English and 2119 meaning through the casing, it is a definition overload, which always creates an opportunity for ambiguity. It’s also important to recognize that it’s much harder to convey 2119 in the spoken word because there isn’t a standard way to read UPPERCASE words in English. After looking at the RFCs, I began to explore the landscape of existing executable specifications and what they could look like.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span>C.-C. Chiang, “TUG: An Executable Specification Language,” in </span><span class="c9">5th IEEE/ACIS International Conference on Computer and Information Science and 1st IEEE/ACIS International Workshop on Component-Based Software Engineering, Software Architecture and Reuse (</span><span class="c9">ICIS-COMSAR’06</span><span class="c9">)</span><span class="c0">, 2006, pp. 180–186. doi: 10.1109/ICIS-COMSAR.2006.85.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c4">DISTILLATION</span><span>: This article describes </span><span class="c9">Tree Unified with Grammar</span><span class="c0">, a programming language for writing specifications that can then be executed like a program. Chiang argues that getting specifications right the first time is of high importance in requirements engineering and believes that more powerful specification tools can ease the burden of requirements engineering. He believes that the existing mechanisms for writing specifications, natural language, and programming languages, are too informal and too concrete respectively for the task, so designed his own mathematical syntax and interpreter for a functional programming language specially designed for writing specifications. TUG’s design centers around a mathematical syntax that describes a finite state machine, a common form of computer program, which pares and combs through an input. Instead of constructing a natural language specification from user requirements and later writing an implementation to verify it, one would write a TUG program and iterate on it in a process similar to prototyping.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c4">CRITIQUE</span><span class="c0">: I agree with Chiang's philosophy behind TUG. I too believe that having executable specifications can significantly ease the software development process, and believe that balancing abstraction with the concreteness of execution is an important part of designing a good system for executable specifications. However, I do not believe that TUG is the right solution for the audience that is the focus of my research: everyday engineers and the executives, designers, and software testers they work with. TUG doesn’t read like a specification or even a mathematical proof; it reads like code, and quite hard code to parse at that, even for someone like me who’s written in a variety of languages and in a functional style for almost three years. For people with beginner or no computer programming knowledge, a TUG specification might come off as a foreign language and exclude them from participating in the software development process. It is ironic that in many cases the “informal” natural language descriptions that precede the sample specifications in the paper describe and solve the problem much more succinctly than TUG itself.</span></p><p class="c5"><span class="c17 c33"></span></p><p class="c7"><span class="c17">I. J. Hayes and C. B. Jones, “Specifications are not (necessarily) executable,” </span><span class="c17 c9">Software Engineering Journal</span><span class="c17">, vol. 4, no. 6, pp. 330–339, 1989.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c4">DISTILLATION</span><span>: Hayes and Jones feel that executable specifications shouldn’t be part of the requirements engineering process. In order to be effective tools for reasoning out the design of systems, specifications must be as abstract as possible and concern themselves with only the behavior of a system, not all the minute details of its implementation. This is in contrast with the concreteness required to make executable specifications executable. Because of the concreteness of executable specifications, it is impossible to describe certain kinds of algorithms such as those with infinite runtimes or ones that can have multiple equivalent answers for a single input, known as non-determinism. Even for deterministic programs with finite runtimes, making their specifications executable can place a burden on the specification writer—for example, there may be many ways to sort a list of elements, but a specification writer should only be concerned about a list being sorted, not </span><span class="c9">how</span><span> it’s sorted—and can result in an extremely slow program due to implementing execution methods such as </span><span class="c9">generate-and-test</span><span class="c0">, where one generates all possible outputs for input and verifies them one by one. Because of their executable nature, engineers may feel encouraged to use executable specifications as a prototype, but this can cause engineers to simply reimplement the structure of the specification when the time to write an implementation comes around instead of writing the most efficient and valid implementation possible.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c4">CRITIQUE</span><span>: I believe that abstraction is an important part of specification writing and software engineering, but most software is already semi-concrete by the time a specification is written; you’re already thinking about approaches to resolving your user requirements and balancing design constraints specific to your system as you’re writing your spec. An executable specification doesn’t need to be able to represent </span><span class="c20">all</span><span> programs; most written software is concerned with being executable and having a single correct answer. Even if a function that is vital to the specification cannot be directly implemented from a specification, we can still generate as much code as possible and then let the user fill in what’s most relevant to their situation. The performance of an executable specification can be bad if it’s property-based, but many specifications in computer science, cooking, medicine, and other fields are </span><span class="c9">instruction-based</span><span>, as in they tell you exactly what to do and how to do it. I believe that this kind of specification will enable us to treat the spec just like a programming language and will translate to efficient machine code. Ultimately, I believe that the benefits of writing a specification that can be executed, such as ease of error checking; closely matching the iterative process of RE; and enabling faster development of implementations—outweigh the cons. The authors suggest an alternative to executable specifications which I want to explore further: a </span><span class="c9">wide-spectrum language</span><span class="c0"> that enables writing specifications and implementing them with a single syntax.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c17">N. E. Fuchs, “Specifications are (preferably) executable,” </span><span class="c17 c9">Software engineering journal</span><span class="c17">, vol. 7, no. 5, pp. 323–334, 1992.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c4">DISTILLATION</span><span class="c0">: Fuchs, in this paper, is in direct opposition of Hayes and Jones. He believes that executable specifications can be a powerful tool for solving one of the greatest challenges in software development: correctness. This is because executable specifications enable engineers to significantly reduce bugs and begin the verification process early in development because of their interactive nature. This interactive nature also allows your user to verify parts of a specification that can’t be formally verified: user experience. To show that these advantages can be kept while still attaining the high levels of abstraction desired by Hayes and Jones, Fuchs rewrites their example specifications in an executable specification language named LSL, showing that only a minimal amount of abstraction needs to be sacrificed to gain the powers of execution. Fuchs argues that true abstraction will never be attainable in specifications written for real-world applications due to specifications being limited not only by executability but also by the user requirements they’re implementing and the mutable nature of mutable user interfaces like filesystems. He does agree that executable specifications will likely be slow but argues that even having a slow specification is much more powerful than one that can’t be executed.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c4">CRITIQUE</span><span class="c0">: Again, I am glad to see that someone shares my vision that executable specifications can be a powerful tool for software development. I originally argued that the levels of abstraction Hayes and Jones desired in their paper weren’t practical for most software developed; the fact that it is possible to achieve both high levels of abstraction and execution at the same time sweetens the deal. The paper has given me two new paths of research to follow. The first is logic programming languages like the one used in the paper, LSL; Fuchs mentions others like Prolog and ML. I believe the ability to state behavior and then derive from that a runnable program is very powerful and may ease specification writing. The second is a technique I plan on using to implement my own grammar: source-to-source transformation. The idea is that we parse code according to grammar, and, instead of directly interpreting it or translating it to machine code, we rewrite the code in another language. This technique can be very powerful as it enables you to create your own language without having to also write an interpreter or compiler.</span></p><h1 class="c2" id="h.7g9hxyg3yysa"><span class="c14">Outline (everything below this heading)</span></h1><h1 class="c2" id="h.rc9faowrpmoh"><span class="c14">Presentation Outline</span></h1><h2 class="c8" id="h.vvx83ccaj9ue"><span>What </span><span class="c9">is</span><span class="c22"> a specification?</span></h2><ul class="c3 lst-kix_l5ek6igvtcm9-0 start"><li class="c6 li-bullet-0"><span class="c0">Making stuff is hard. Like, really, really hard.</span></li><li class="c6 li-bullet-0"><span class="c0">We need others to help make our ideas a reality.</span></li><li class="c6 li-bullet-0"><span class="c0">There’s one problem though: how do we effectively communicate our ideas?</span></li><li class="c6 li-bullet-0"><span class="c0">when a baker and a client are communicating about how a cake is to be made, the baker may create an interim recipe that both they and the client can evaluate</span></li><li class="c6 li-bullet-0"><span class="c0">first, a client tells the baker what they need from the cake—3 tiers, chocolate cake, strawberry frosting, gluten-free—and lets the baker worry sweat the details (user requirements)</span></li><li class="c6 li-bullet-0"><span class="c0">the baker with those requirements designs a cake, drawing out its shape, creating a list of ingredients, and writing up decoration instructions (specification)</span></li><li class="c6 li-bullet-0"><span class="c0">the baker then shares their specification with the client, making sure that the users’ requirements are met; for example, the baker may realize they didn’t set enough ingredients aside for the user’s desired serving size, or the client may realize that they actually need the cake to be vegan, even though they didn’t initially mention it (validation)</span></li><li class="c6 li-bullet-0"><span class="c0">the baker then uses their specification, now revised and validated, to actually go bake a cake (implementation)</span></li><li class="c6 li-bullet-0"><span class="c0">the client then validates the implementation, making sure that it follows the baker’s specification and the client’s own requirements (verification)</span></li><li class="c6 li-bullet-0"><span class="c0">this set of interactions between the baker and their client is very similar to how programmers coordinate writing software with their clients and one another</span></li><li class="c6 li-bullet-0"><span class="c0">this form of engineering, called requirements engineering, prioritizes the clear communication of behavior over the fine details of implementing software, making it for engineers to coordinate on large software projects</span></li></ul><h2 class="c8" id="h.g07yjsvzh6dn"><span class="c22">Formal vs. Informal</span></h2><ul class="c3 lst-kix_o50dswdx9e7q-0 start"><li class="c6 li-bullet-0"><span class="c0">well, now we have a tool for communicating our ideas; but how do we use it well?</span></li><li class="c6 li-bullet-0"><span class="c0">in the case of a recipe, there is a single way to write one: in the natural language of your choosing</span></li><li class="c6 li-bullet-0"><span class="c0">for computers, however, there is a significant divide in the CS community</span></li><li class="c6 li-bullet-0"><span class="c0">there are two kinds of specifications one can write: natural language specs and formal specs.</span></li><li class="c6 li-bullet-0"><span class="c0">natural language specifications are very similar to recipes: they use plain English with computer jargon to communicate the procedures of a program</span></li><li class="c6 li-bullet-0"><span class="c0">however, due to the many intricacies of natural language, which we’ll discuss later, most computer scientists find natural language unsuitable for exhaustively and clearly communicating how a program ought to function</span></li><li class="c6 li-bullet-0"><span class="c0">this doesn’t stop natural language from being the primary way programmers communicate: the specifications for famous internet protocols like TCP and UDP, web browsers, and even entire operating systems like POSIX Unix are all described using natural language</span></li><li class="c6 li-bullet-0"><span class="c0">on the other hand, we have formal specifications; they’re written in precise notations inspired by discrete mathematics and programming languages that do exhaustively describe the functioning of a program</span></li><li class="c6 li-bullet-0"><span class="c0">formal specifications are extremely powerful but have seen limited adoption in the industry because of their complexity, significant barrier to entry, and incomprehensibility to non-programmers</span></li><li class="c6 li-bullet-0"><span class="c0">as you may guess, formal specifications are named as such because everyone presumes mathematical syntax is the only way to fully describe a program</span></li><li class="c6 li-bullet-0"><span class="c0">however, I believe that the concepts of a formal specification and natural language specification can be married in such a way that we prevent our mission-critical software from having bugs at the conceptual level while not being exclusionary</span></li><li class="c6 li-bullet-0"><span class="c0">this is the goal of my presentation: to explore a world where formal natural-language specifications exist</span></li><li class="c6 li-bullet-0"><span class="c0">so, let’s design one!</span></li></ul><h2 class="c8" id="h.1ktrci3udn35"><span class="c22">Building It</span></h2><ul class="c3 lst-kix_82er1brroaog-0 start"><li class="c6 li-bullet-0"><span>As part of my presentation, I have written a description of a possible formal natural specification language named </span><span class="c9">Gorr</span><span class="c0">. We will go through the specification together, highlighting my design decisions and how I have avoided the informal trappings of natural language.</span></li><li class="c6 li-bullet-0"><span class="c0">Gorr, like all languages, has a grammar. Its 66-line grammar is written in Extended Backus-Naur Form, or EBNF, a grammar commonly used by computer scientists to specify the grammar of programming languages and protocols.</span></li><li class="c6 li-bullet-0"><span class="c0">There are two very important implications that come with Gorr being able to be represented in EBNF:</span></li></ul><ol class="c3 lst-kix_82er1brroaog-1 start" start="1"><li class="c7 c11 li-bullet-0"><span class="c0">Gorr can be parsed by a computer, which makes the automatic linting, verification, and even execution of a Gorr specification possible, among a litany of other ideas.</span></li><li class="c7 c11 li-bullet-0"><span class="c0">Any grammar written in EBNF is a formal grammar. The fact that Gorr has a fully defined structure almost entirely eliminates concerns about ambiguity. There is only one way to parse a Gorr specification. I will later show how this also helps with proving that there is only one way to interpret a Gorr specification.</span></li></ol><ul class="c3 lst-kix_82er1brroaog-0"><li class="c6 li-bullet-0"><span class="c0">Our language will have two data types: the integer and the Boolean.</span></li></ul><ul class="c3 lst-kix_pqyspzcpl1nw-0 start"><li class="c6 li-bullet-0"><span class="c0">An integer is a whole number that is positive, negative, or zero; for example, -2, 5, and 3 are integers.</span></li><li class="c6 li-bullet-0"><span class="c0">Booleans are a lot like light switches: they can be either on or off. In our case, we represent those states with the words true and false</span></li><li class="c6 li-bullet-0"><span class="c0"> Note that this description only describes the behavior of the data types just enough that we can use them in our specifications; the representation of these data types in memory is up to the implementer of our specification, not us. This abstraction is one of the powers of specifications.</span></li><li class="c6 li-bullet-0"><span class="c0">Also, note how the description of these data types is not extremely rigorous; like in all other industries, computer scientists use warrants and assumed knowledge so that they don’t have to include a rigorous proof for the set of integers at the beginning of every specification.</span></li><li class="c6 li-bullet-0"><span class="c0">In our language, integers must always be literally represented with Arabic numerals and an optional hyphen-minus signifying negation; -2 is semantically different from negative two. This may seem like an over-specification, but this is necessary in order to avoid ambiguity.</span></li><li class="c6 li-bullet-0"><span class="c0">Similarly, Booleans must always be represented with the sequences of letters true and false; true is semantically different from on, True, or yes.</span></li><li class="c6 li-bullet-0"><span class="c0">We can manipulate these data types with operators. For integers, we have the four arithmetic operators, and Booleans the most basic operations AND, OR, and NOT. They both share an operation for equivalence.</span></li><li class="c6 li-bullet-0"><span class="c0">The operations use language similar to that of mathematicians. Although they are a tad verbose, I have opted to not use mathematical symbols in this language for readability. In an actual specification language, I would only use mathematical symbols for terseness.</span></li><li class="c6 li-bullet-0"><span class="c0">We can then store these manipulations in variables for later access and further manipulation, making sure that we tell the variable what kind of value it can store alongside an initial value.</span></li><li class="c6 li-bullet-0"><span class="c0">Because Gorr has only two types and is statically typed, meaning the value of a variable cannot be changed, we avoid contradictions that arise from implicit transformations of data and the wishful thinking of “there must be a data structure that perfectly represents my problem, so I’ll just use it without explaining it.”</span></li><li class="c6 li-bullet-0"><span class="c0">Variables in Gorr must be declared before they can be used; this prevents forward references and use of variables that don’t exist, which can cause silence.</span></li><li class="c6 li-bullet-0"><span class="c0">Finally, we can encapsulate a series of value manipulations inside of an algorithm, taking in a list of values as arguments and then returning a value to be used later. Actions taken inside of an algorithm are numbered, with these numbers increasing as statements nest.</span></li><li class="c6 li-bullet-0"><span class="c0">Gorr has the two most simple forms of control flow: an if-otherwise statement and a while statement.</span></li><li class="c6 li-bullet-0"><span class="c0">If the expression of a while statement evaluates to true, the inner statements will be executed, and will continue to be executed until the expression is equal to false. If the expression of an if-otherwise statement is true, only the statements inside the if statement will run. Otherwise, the statements inside the otherwise statement will run.</span></li><li class="c6 li-bullet-0"><span class="c0">This example also demonstrates the pass statement, which does absolutely nothing; use it if you only are about an expression being true.</span></li><li class="c6 li-bullet-0"><span class="c0">Did I mention that Gorr has two data types? It actually has one more that can only be used as the return value type for an algorithm, meaning you can’t store it in a variable: void. It has no literal syntax, but can be generated by a return statement with no expression. You can only do one thing with a void value: discard it. This is useful for Gorr specifications that want to represent side effects such as printing to a console.</span></li><li class="c6 li-bullet-0"><span class="c0">With that, our tour of Gorr is complete; for more information, a complete grammar of the language, and some example programs, see the informal description of the language I’ve handed out.</span></li></ul><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">Cutting room floor: One consequence of this design decision is that I had to make most of the mathematical and logical operations use prefix notation in order to avoid the parsing ambiguity of statements like “3 plus 4 divided by 7,” which can result either in 3 [ 3 + (4 / 7) ] or 1 [ (3 + 4) / 7 ].</span></p><h2 class="c8" id="h.wdeon7bjhaht"><span class="c22">How My Approach Addresses Previous Issues with Natural Language</span></h2><ul class="c3 lst-kix_bwcnx74ykyp6-0 start"><li class="c6 li-bullet-0"><span class="c0">Let’s now see how Gorr addresses the major issues the specification community has with natural language; I’ve name-dropped a few throughout explaining Gorr, but we’ll address them all at once here.</span></li><li class="c6 li-bullet-0"><span class="c0">In his highly cited 1985 article “On Formalism and Specifications,” Bertrand Meyer argues against the use of natural language in formal specification, centering his argument around “the seven sins of the specifier.” We will look at all seven and see how Gorr addresses them.</span></li><li class="c6 li-bullet-0"><span class="c0">noise: text that is irrelevant to describing the algorithm at hand</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-1 start"><li class="c7 c11 li-bullet-0"><span>Gorr is a limited subset of the English language expressly designed for writing specifications. As such, a valid Gorr program can </span><span class="c9">only</span><span class="c0"> describe the outline of an algorithm and nothing else. For example, in a Python program, it is impossible for one to go on and on about a problem in a way that is actually executed; this is because Python is a programming language, not a public forum.</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-0"><li class="c6 li-bullet-0"><span class="c0">silence: a feature of a problem goes unspecified</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-1 start"><li class="c7 c11 li-bullet-0"><span class="c0">Many of Gorr’s features prevent one from performing omission, including:</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-2 start"><li class="c7 c13 li-bullet-0"><span class="c0">static typing,</span></li><li class="c7 c13 li-bullet-0"><span class="c0">variable initialization on declaration, and</span></li><li class="c7 c13 li-bullet-0"><span class="c0">variables and functions needing to be declared before they can be used</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-0"><li class="c6 li-bullet-0"><span class="c0">over-specification: specifying a solution to the problem instead of the problem itself</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-1 start"><li class="c7 c11 li-bullet-0"><span>Gorr avoiding this sin is more of an opinion than an assertion. Many formal specification languages prefer a compositional approach, using sets and filters on those sets to narrow down toward a solution. Gorr instead uses an algorithmic approach, telling developers what their implementations </span><span class="c9">must</span><span class="c0"> do in order to be valid; this approach will be more familiar to those already writing natural language specifications in the industry. I believe I soothe Meyer’s concerns a little by creating intentionally abstract definitions for data types, but he may believe that the algorithmic approach is itself an over-specification. I believe both are valid.</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-0"><li class="c6 li-bullet-0"><span class="c0">contradiction: two elements of a specification are at odds with one another</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-1 start"><li class="c7 c11 li-bullet-0"><span class="c0">The main example of contradiction Meyer brings up in the article is a specification changing the types of variables in the middle of a specification; this is not possible because of Gorr’s strictly typed nature.</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-0"><li class="c6 li-bullet-0"><span class="c0">ambiguity: there are multiple ways to interpret a part of a specification</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-1 start"><li class="c7 c11 li-bullet-0"><span class="c0">Gorr prevents ambiguity in two ways. The first is its grammar: there is only one way to parse Gorr. The second is its description: because Gorr redefines parts of the English language to match the context of a specification, Gorr gives the reader only one way to interpret what they have parsed. These two elements come together to create a near-bulletproof shield against ambiguity, with the only possible chinks being in the language’s description.</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-0"><li class="c6 li-bullet-0"><span class="c0">forward reference: something is referenced before it is defined</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-1 start"><li class="c7 c11 li-bullet-0"><span class="c0">This is not possible in Gorr due to the language requiring variables and functions be defined before they’re used.</span></li><li class="c7 c11 li-bullet-0"><span class="c0">I will note that is possible to have forward references in programming languages, which are universally believed to be formal, such as JavaScript; it doesn’t change the fact that forward references are confusing.</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-0"><li class="c6 li-bullet-0"><span class="c0">wishful thinking: the problem is defined in such a way that an implementation cannot be realistically verified</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-1 start"><li class="c7 c11 li-bullet-0"><span class="c0">Because one is limited to the constructs of the language when writing a Gorr specification, you can’t define behavior that cannot be accomplished with the specification language, meaning that implementation can still be verified.</span></li><li class="c7 c11 li-bullet-0"><span class="c0">I will note that this sin is the most weakly defined and that formal verification is very much not a solved problem in computer science; there are cases of implementations of valid specifications that cannot be trivially verified.</span></li></ul><h2 class="c8" id="h.a34fdz1oqkad"><span class="c22">Why Natural Language?</span></h2><ul class="c3 lst-kix_36o98skmki7a-0 start"><li class="c6 li-bullet-0"><span class="c0">Alright! It seems like we’re really onto something here. As this presentation begins to wind down, I think it’s important that our specification answers two important questions, the first being “why natural language?”</span></li><li class="c6 li-bullet-0"><span class="c0">I cling to natural language for the same reason everyone does: it’s universal</span></li><li class="c6 li-bullet-0"><span class="c0">Anyone, with a little bit of training, can parse them to know they’re correct, including users, QAs, executives, designers, and anyone else who may lack technical expertise.</span></li><li class="c6 li-bullet-0"><span class="c0">we communicate in all other disciplines in natural language, so why should computers be the exception?</span></li><li class="c6 li-bullet-0"><span class="c0">lowering the barrier to writing correct software easier is critical as technology more and more defines our world</span></li></ul><h2 class="c8" id="h.kkyq1gl7ovh1"><span class="c22">If This Is Possible, Why Does Everyone Say It Isn’t?</span></h2><ul class="c3 lst-kix_ooiavzuaqt14-0 start"><li class="c6 li-bullet-0"><span>the second question that needs answering is, “well, if this </span><span class="c9">is</span><span> possible </span><span class="c9">and</span><span class="c0"> it makes sense, how come a lot of people much smarter and more experienced than you say it isn’t?”</span></li><li class="c6 li-bullet-0"><span class="c0">I think the issue is that people haven’t found the Goldilocks zone for the amount of freedom natural language gets in computer science yet.</span></li><li class="c6 li-bullet-0"><span class="c0">Programming languages like HyperCard, AppleScript, and SQL make use of natural language to represent computation in a form accessible to many. The issue is that these languages have limited domains; the natural language in a sense has too little freedom in order to express any arbitrary computation. One issue with AppleScript is that the syntax used for commands is usually defined by a third-party, meaning that in effect that AppleScript contains many small languages that all subtly clash with each other.</span></li><li class="c6 li-bullet-0"><span class="c0">On the other hand, there are people who want to derive computational meaning out of *any* utterance; this can be seen in tools like OpenAI’s GPT series of language models.</span></li><li class="c6 li-bullet-0"><span class="c0">Trying to extract meaning from any sentence is extremely difficult. While languages like English do have formal grammars, their grammars are large, and the process of then interpreting those parsed trees is another story entirely. Meyer’s seven sins don’t just describe why it’s hard to parse natural language specifications, but why it’s hard to parse almost natural language anything.</span></li><li class="c6 li-bullet-0"><span class="c0">I believe Gorr, with its context-free grammar and controlled-language-like restrictions strikes a nice balance between the two. Hopefully, we’ll see proper languages that inherit the ideas of Gorr someday so that specification writing can be made that little bit easier.</span></li></ul><h2 class="c8" id="h.zfvgaqpnu7y3"><span class="c9">The Gorr Specification Language</span></h2><h3 class="c19" id="h.vbb1rcks9bk"><span class="c15">Expressions</span></h3><h3 class="c19" id="h.6beane8sv70p"><span class="c15">Data Types</span></h3><p class="c7"><span class="c0">The Gorr language has three data types: the integer, the Boolean, and void. Integers in Gorr are signed. The void type is used to signify a function that doesn’t return a value; a variable, when declared, cannot be of type void, and by extension cannot be assigned the return value of a void function call.</span></p><h3 class="c19" id="h.qx1kgrdl18b2"><span class="c15">Operations</span></h3><p class="c7"><span class="c0">Integers in our language have six operations—negation, addition, subtraction, multiplication, division, and modulo—that all result in integers.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span>In the case of division, because Gorr lacks fractional numbers, the quotient returned discards the remainder; for example, </span><span class="c9">the division of 5 by 2</span><span class="c0"> does not result in 2 ½, but instead 2. If one wanted the remainder of 1, they could instead use the modulo operation.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span>Booleans have three operations—</span><span class="c9">NOT</span><span>, </span><span class="c9">AND</span><span>, and </span><span class="c9">OR</span><span>—that result in booleans.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">Integers have four comparison operators—greater than, greater than or equal to, less than, and less than or equal to—that result in Booleans.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span>Integers and Booleans share one comparison operator, equivalence, resulting in a Boolean. The equivalence operator </span><span class="c9">must not</span><span class="c0"> be used to test the equivalence of two different data types; a specification that tries to equate an integer to a Boolean is invalid.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">All operators are evaluated from left to right; Gorr has no operator precedence.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">The Boolean, integer, and void types all share one operation that comes in the form of a statement: discard. This can be used to make a function call and dispose of the value.</span></p><h3 class="c19" id="h.qbvztxqd1ddw"><span class="c15">Variables</span></h3><p class="c7"><span>A variable can be used to remember a value and retrieve it at a later time. Variable types are static; for example, initializing an integer variable with a boolean is invalid. Variables </span><span class="c9">must</span><span class="c0"> be initialized at declaration.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">Variables declared outside of functions are constant and cannot be re-assigned.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span>Variables declared outside of functions have a global scope; they are accessible from any future variable or algorithm declarations. Variables inside of a function or a control flow statement have a local scope. Once an algorithm ends, the variables declared inside are no longer accessible; variables declared in one algorithm cannot be accessed from another. Once an </span><span class="c23">If</span><span> statement or </span><span class="c23">While</span><span> statement ends, the variable is </span><span class="c9">freed</span><span class="c0"> and can be used again in the algorithm.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span>Specification writers </span><span class="c9">should not</span><span> use lone value literals as names for variables; while </span><span class="c23">[[ true ]]</span><span> and </span><span class="c23">true</span><span class="c0"> are semantically different in Gorr, it may be hard for human readers to parse.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">A variable cannot be referenced before it is declared.</span></p><h3 class="c19" id="h.bjzl4b2e5k6t"><span class="c15">Algorithms</span></h3><p class="c7"><span class="c0">Algorithms in Gorr are used to encapsulate logic. They optionally can take a number of arguments and must have a return type.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span>A function </span><span class="c9">must</span><span class="c0"> have a return statement at the end of all branches.</span></p><h3 class="c19" id="h.ki6bfuc35waa"><span class="c15">Control Flow</span></h3><p class="c7"><span class="c0">An algorithm has access to four forms of control flow:</span></p><ul class="c3 lst-kix_5qumemskpxo9-0 start"><li class="c6 li-bullet-0"><span class="c0">the while loop repeatedly executes the statements inside it until its condition is false</span></li><li class="c6 li-bullet-0"><span class="c0">the if-otherwise statement executes the if branch if the condition is true, otherwise the otherwise branch is executed.</span></li><li class="c6 li-bullet-0"><span class="c0">The return statement ends the execution of a algorithm, and optionally returns a non-void value.</span></li><li class="c6 li-bullet-0"><span class="c0">The pass statement does nothing; it’s useful for if-otherwise statements where one only wants something to happen in the if.</span></li></ul><p class="c5"><span class="c0"></span></p><p class="c7"><span>An otherwise statement </span><span class="c9">must </span><span class="c0">always come after an if statement.</span></p><p class="c5"><span class="c0"></span></p><hr style="page-break-before:always;display:none;"><h3 class="c19 c24" id="h.et0u52wexzyr"><span class="c15"></span></h3><h3 class="c19" id="h.8hxzdijaut52"><span class="c15">Examples</span></h3><h4 class="c21" id="h.4l1u622bdkmi"><span class="c10">Factorial</span></h4><p class="c7"><span class="c0">The algorithm [[ factorial ]], with the signature integer [[a]] returns integer, does the following:</span></p><p class="c7"><span class="c0">1. If either [[a]] is equal to 0 or [[a]] is equal to 1,</span></p><p class="c7"><span class="c0">1.1. Return 1.</span></p><p class="c7"><span class="c0">2. Otherwise,</span></p><p class="c7"><span class="c0">2.1. Return the multiplication of [[a]] by call [[factorial]] arguments the subtraction of 1 from [[a]].</span></p><h4 class="c21" id="h.1rulurusfydk"><span class="c16"><a class="c18" href="https://www.google.com/url?q=https://rosettacode.org/wiki/Greatest_common_divisor%23Python&sa=D&source=editors&ust=1691984934396237&usg=AOvVaw1fyXyli3WVImhTCzEFzKm7">Greatest Common Denominator</a></span><span> and </span><span class="c16"><a class="c18" href="https://www.google.com/url?q=https://rosettacode.org/wiki/Least_common_multiple%23Python&sa=D&source=editors&ust=1691984934396588&usg=AOvVaw3nHtZTMwUiH4lCkA2-Ova0">Least Common Multiple</a></span></h4><p class="c7"><span class="c0">The algorithm [[ absolute value ]] with the signature integer [[ a ]] returns integer, does the following:</span></p><p class="c7"><span class="c0">1. If [[ a ]] is greater than or equal to 0,</span></p><p class="c7 c12"><span class="c0">1.1. Return [[ a ]].</span></p><p class="c7"><span class="c0">2. Otherwise,</span></p><p class="c7 c12"><span class="c0">2.1. Return the negation of [[ a ]].</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">The algorithm [[ greatest common denominator ]] with the signature integer [[ u ]], integer [[ v ]] returns integer, does the following:</span></p><p class="c7"><span class="c0">1. While [[ v ]] is greater than 0,</span></p><p class="c7 c12"><span class="c0">1.1. The integer [[ previous u ]] is [[ u ]].</span></p><p class="c7 c12"><span class="c0">1.2. Set [[ u ]] to [[ v ]].</span></p><p class="c7 c12"><span class="c0">1.3. Set [[ v ]] to the modulo of [[ previous u ]] by [[ v ]].</span></p><p class="c7"><span class="c0">2. Return call [[ absolute value ]] arguments [[ u ]].</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">The algorithm [[ least common multiple ]] with the signature integer [[ u ]], integer [[ v ]] returns integer, does the following:</span></p><p class="c7"><span class="c0">1. If both [[ u ]] is greater than 0 and [[ a ]] is greater than 0,</span></p><p class="c7 c12"><span class="c0">1.1. Return the division of call [[ absolute value ]] arguments the multiplication of [[ a ]] by [[ b ]] by call [[ greatest common denominator ]] arguments [[ u ]], [[ v ]].</span></p><p class="c7"><span class="c0">2. Otherwise,</span></p><p class="c7 c12"><span class="c0">2.1. Return 0.</span></p><hr style="page-break-before:always;display:none;"><h3 class="c19 c24" id="h.gky4t8632qj5"><span class="c15"></span></h3><h3 class="c19" id="h.kvqw7xbx8pb"><span class="c15">Grammar</span></h3><p class="c7"><span class="c0">The formal context-free grammar for Gorr, notated in Extended Backus-Naur Form, is listed below:</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">(* Utility non-terminals. *)</span></p><p class="c7"><span class="c0">⟨text⟩ → ? a string of characters that doesn’t have “[[” or “]]” as substrings ?;</span></p><p class="c7"><span class="c0">⟨space⟩ → (“ “ | “\t”)+;</span></p><p class="c7"><span class="c0">⟨newline⟩ → “\n”;</span></p><p class="c7"><span class="c0">⟨period⟩ → “.”;</span></p><p class="c7"><span class="c0">⟨comma⟩ → “,”</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">(* Value literals. *)</span></p><p class="c7"><span class="c0">⟨digit⟩ → “0” | “1” | “2” | “3” | “4” | “5” | “6” | “7” | “8” | “9” | “0”;</span></p><p class="c7"><span class="c0">⟨integer⟩ → “-”? ⟨digit⟩+;</span></p><p class="c7"><span class="c0">⟨boolean⟩ → “true” | “false”;</span></p><p class="c7"><span class="c0">⟨value⟩ → ⟨integer⟩ | ⟨boolean⟩;</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span>(* Operations. All in </span><span class="c16"><a class="c18" href="https://www.google.com/url?q=https://en.wikipedia.org/wiki/Polish_notation&sa=D&source=editors&ust=1691984934398759&usg=AOvVaw0fVWYJQ7X0uQTYkm4ymI7i">prefix notation</a></span><span class="c0"> except equality. *)</span></p><p class="c7"><span class="c0">⟨negation⟩ → “the negation of” ⟨space⟩ ⟨expression⟩;</span></p><p class="c7"><span class="c0">⟨not⟩ → “not” ⟨space⟩ ⟨expression⟩;</span></p><p class="c7"><span class="c0">⟨unary operation⟩ → ⟨negation⟩ | ⟨not⟩;</span></p><p class="c7"><span class="c0">⟨addition⟩ → “the addition of” ⟨space⟩ ⟨expression⟩ ⟨space⟩ “and” ⟨space⟩ ⟨expression⟩;</span></p><p class="c7"><span class="c0">⟨subtraction⟩ → “the subtraction of” ⟨space⟩ ⟨expression⟩ ⟨space⟩ “from” ⟨space⟩ ⟨expression⟩;</span></p><p class="c7"><span class="c0">⟨multiplication⟩ → “the multiplication of” ⟨space⟩ ⟨expression⟩ ⟨space⟩ “by” ⟨space⟩ ⟨expression⟩;</span></p><p class="c7"><span class="c0">⟨multiplication⟩ → “the division of” ⟨space⟩ ⟨expression⟩ ⟨space⟩ “by” ⟨space⟩ ⟨expression⟩;</span></p><p class="c7"><span class="c0">⟨modulo⟩ → “the modulo of” ⟨space⟩ ⟨expression⟩ ⟨space⟩ “by” ⟨space⟩ ⟨expression⟩;</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">⟨and⟩ → “both” ⟨space⟩ ⟨expression⟩ ⟨space⟩ “and” ⟨expression⟩;</span></p><p class="c7"><span class="c0">⟨or⟩ → “either” ⟨space⟩ ⟨expression⟩ ⟨space⟩ “or” ⟨expression⟩;</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">⟨greater than or equal to⟩ → ⟨expression⟩ ⟨space⟩ “is greater than or equal to” ⟨space⟩ ⟨expression⟩;</span></p><p class="c7"><span class="c0">⟨greater than⟩ → ⟨expression⟩ ⟨space⟩ “is greater than” ⟨space⟩ ⟨expression⟩;</span></p><p class="c7"><span class="c0">⟨less than than or equal to⟩ → ⟨expression⟩ ⟨space⟩ “is less than or equal to” ⟨space⟩ ⟨expression⟩;</span></p><p class="c7"><span class="c0">⟨less than⟩ → ⟨expression⟩ ⟨space⟩ “is less than” ⟨space⟩ ⟨expression⟩;</span></p><p class="c7"><span class="c0">⟨equality⟩ → ⟨expression⟩ ⟨space⟩ “is equal to” ⟨space⟩ ⟨expression⟩;</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">⟨binary operation⟩ → ⟨addition⟩ | ⟨subtraction⟩ | ⟨multiplication⟩ | ⟨division⟩ | ⟨modulo⟩ | ⟨and⟩ | ⟨or⟩ | ⟨greater than or equal to⟩ | ⟨greater than⟩ | ⟨less than or equal to⟩ | ⟨less than⟩ | ⟨equality⟩;</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">⟨operation⟩ → ⟨unary operation⟩ | ⟨binary operation⟩;</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">(* Leading and trailing spaces in the variable name are consumed by the parser. *)</span></p><p class="c7"><span class="c0">⟨variable⟩ → “[[” ⟨space⟩? ⟨text⟩ ⟨space⟩? “]]”;</span></p><p class="c7"><span class="c0">⟨algorithm call⟩ → “call” ⟨space⟩ ⟨variable⟩ (“arguments” ⟨space⟩ ⟨expression⟩ (⟨comma⟩ ⟨space⟩ ⟨expression⟩)*)?;</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">⟨expression⟩ → ⟨operation⟩ | ⟨algorithm call⟩ | ⟨value⟩ | ⟨variable⟩;</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">(* Statements. *)</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">⟨data type⟩ → “integer” | “Boolean”;</span></p><p class="c7"><span class="c0">⟨variable declaration⟩ → “The” ⟨space⟩ ⟨data type⟩ ⟨space⟩ ⟨variable⟩ ⟨space⟩ “is” ⟨expression⟩ ⟨period⟩;</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">⟨variable assignment⟩ → “Set” ⟨space⟩ ⟨variable⟩ ⟨space⟩ “to” ⟨space⟩ ⟨expression⟩ ⟨period⟩;</span></p><p class="c7"><span class="c0">⟨if⟩ → “If” ⟨space⟩ ⟨expression⟩ ⟨comma⟩;</span></p><p class="c7"><span class="c0">⟨otherwise⟩ → “Otherwise” ⟨comma⟩;</span></p><p class="c7"><span class="c0">⟨while⟩ → “While” ⟨space⟩ ⟨expression⟩ ⟨comma⟩;</span></p><p class="c7"><span class="c0">⟨return⟩ → “Return” (⟨space⟩ ⟨expression⟩)? ⟨period⟩;</span></p><p class="c7"><span class="c0">⟨discard⟩ → “Discard” ⟨space⟩ ⟨expression⟩ ⟨period⟩;</span></p><p class="c7"><span class="c0">⟨pass⟩ → “Pass” ⟨period⟩;</span></p><p class="c7"><span class="c0">⟨algorithm statement⟩ → ⟨if⟩ | ⟨otherwise⟩ | ⟨while⟩ | ⟨return⟩ | ⟨variable declaration⟩ | ⟨variable assignment⟩ | ⟨discard⟩ | ⟨pass⟩;</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">(* Algorithms. *)</span></p><p class="c7"><span class="c0">⟨algorithm declaration⟩ → “The algorithm” ⟨space⟩ ⟨variable⟩ ⟨space⟩ ⟨comma⟩</span></p><p class="c7 c12"><span class="c0">(* Arguments*)</span></p><p class="c7 c12"><span class="c0">“with the signature” ( ⟨data type⟩ ⟨space⟩ ⟨variable⟩ (⟨comma⟩ ⟨space⟩ ⟨data type⟩ ⟨space⟩ ⟨variable⟩)*)? “returns” (⟨data type⟩ | “void”) ⟨comma⟩</span></p><p class="c7 c12"><span class="c0">“does the following:” ⟨newline⟩</span></p><p class="c7 c12"><span class="c0">(* Body *)</span></p><p class="c7 c12"><span class="c0">(<space>? ⟨digit⟩+ (⟨period⟩ ⟨digit⟩)* ⟨period⟩ ⟨space⟩ ⟨algorithm statement⟩ ⟨newline⟩)+;</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">(* Specification *)</span></p><p class="c7"><span class="c0">⟨statement⟩ → (⟨variable declaration⟩ | ⟨algorithm declaration⟩) ⟨newline⟩;</span></p><p class="c7"><span class="c0">⟨specification⟩ → ⟨statement⟩+;</span></p><h1 class="c2" id="h.svf3lxfpt82d"><span class="c14">Research Question</span></h1><p class="c7"><span class="c0">How can natural language be formalized to make the process of writing specifications for complex software easier?</span></p><h1 class="c2" id="h.lfz4b0obbpkv"><span class="c14">Introduction and Claim</span></h1><p class="c7"><span class="c0">As cool as computer science is, it is not a one-on-one conversation with the machine. It’s a collaborative process that for the most part takes place outside the text editor. When dozens of people are all working towards the development of a single product, all of them sharing different literacy in computer programming and user design, they need a guiding force. That is the purpose of the specification. However, specifications can be hard to understand, and even lead to bugs and implementation differences, the things they’re meant to avoid. Natural language specifications can be challenging to write clearly, and formal specifications, usually relying on mathematical syntax, can be challenging to parse for the uninitiated.</span></p><p class="c5"><span class="c0"></span></p><p class="c7"><span class="c0">In this presentation, I aim to show that the benefits of both informal natural language specifications and formal mathematical specifications can be combined with minimal downsides, while at the same time allowing said specifications to be read by both humans and computers. By writing in this ideal specification language, engineers can write specifications that can be read and verified by anyone with the appropriate domain knowledge and turned into an executable program, creating a single source of truth for an application. This can be accomplished through extremely restricted prescriptive grammar. Through this, specifications can be easily parsed by computers and humans can avoid ambiguity when interpreting them.</span></p><h1 class="c2" id="h.kavpay4fl9bt"><span class="c14">Background</span></h1><h2 class="c8" id="h.bhbsa1p7vzq7"><span class="c22">The Requirements Engineering Process</span></h2><p class="c7"><span>heavily pulls from </span><span class="c16"><a class="c18" href="https://www.google.com/url?q=https://www.researchgate.net/profile/Ikram-Asghar/publication/281645652_An_Empirical_Study_of_Software_Requirements_Verification_and_Validation_Techniques_along_their_Mitigation_Strategies/links/55f2a17008ae199d47c4841c/An-Empirical-Study-of-Software-Requirements-Verification-and-Validation-Techniques-along-their-Mitigation-Strategies.pdf&sa=D&source=editors&ust=1691984934402717&usg=AOvVaw05quU3yWCx6DtgT7WXVzmf">Khan et al., 2015</a></span></p><ul class="c3 lst-kix_kt1x3xteemmb-0 start"><li class="c6 li-bullet-0"><span class="c0">requirements engineering: an engineering pattern centered around learning, processing, and acting on a user’s needs for a piece of software</span></li></ul><ul class="c3 lst-kix_kt1x3xteemmb-1 start"><li class="c7 c11 li-bullet-0"><span class="c26">“an area of software engineering concerned with the acquisition, analysis, specification, validation, and management of software requirements”</span><span class="c0"> (Abran et al., 2001)</span></li></ul><ul class="c3 lst-kix_kt1x3xteemmb-0"><li class="c6 li-bullet-0"><span class="c0">user requirements</span></li></ul><ul class="c3 lst-kix_kt1x3xteemmb-1 start"><li class="c7 c11 li-bullet-0"><span class="c0">a rough outline of a desired product from the perspective of the user</span></li><li class="c7 c11 li-bullet-0"><span>it describes what they want to be able to do, </span><span class="c9">not</span><span class="c0"> how to do it</span></li><li class="c7 c11 li-bullet-0"><span class="c0">analogy: “I want a chocolate cake with a serving size of 12 people”</span></li></ul><ul class="c3 lst-kix_kt1x3xteemmb-0"><li class="c6 li-bullet-0"><span class="c0">specification</span></li></ul><ul class="c3 lst-kix_kt1x3xteemmb-1 start"><li class="c7 c11 li-bullet-0"><span class="c0">a specification is an abstract design for assuring the user requirements are fulfilled</span></li><li class="c7 c11 li-bullet-0"><span class="c0">analogy: a recipe for baking said cake</span></li></ul><ul class="c3 lst-kix_kt1x3xteemmb-0"><li class="c6 li-bullet-0"><span class="c0">verification</span></li></ul><ul class="c3 lst-kix_kt1x3xteemmb-1 start"><li class="c7 c11 li-bullet-0"><span class="c0">make sure the specification both implements the user requirements and is correct</span></li><li class="c7 c11 li-bullet-0"><span class="c0">analogy:</span></li></ul><ul class="c3 lst-kix_kt1x3xteemmb-2 start"><li class="c7 c13 li-bullet-0"><span class="c0">make sure the cake is chocolate, not gold</span></li><li class="c7 c13 li-bullet-0"><span class="c0">assert the recipe contains enough ingredients to fulfill the serving size in the user's requirements</span></li></ul><ul class="c3 lst-kix_kt1x3xteemmb-0"><li class="c6 li-bullet-0"><span class="c0">implementation</span></li></ul><ul class="c3 lst-kix_kt1x3xteemmb-1 start"><li class="c7 c11 li-bullet-0"><span class="c0">the specification put into practice</span></li><li class="c7 c11 li-bullet-0"><span class="c0">an actual piece of software</span></li><li class="c7 c11 li-bullet-0"><span class="c0">analogy: the cake is baked using a recipe as a guide</span></li></ul><ul class="c3 lst-kix_kt1x3xteemmb-0"><li class="c6 li-bullet-0"><span class="c0">validation</span></li></ul><ul class="c3 lst-kix_kt1x3xteemmb-1 start"><li class="c7 c11 li-bullet-0"><span class="c0">make sure the implementation actually implements the specification</span></li><li class="c7 c11 li-bullet-0"><span class="c0">user inspects baked cake to make sure it follows initial requirements and recipe; don’t want an over/undercooked cake</span></li></ul><ul class="c3 lst-kix_kt1x3xteemmb-0"><li class="c6 li-bullet-0"><span class="c0">formality: how precise is the language you’re using to describe a specification</span></li></ul><ul class="c3 lst-kix_kt1x3xteemmb-1 start"><li class="c7 c11 li-bullet-0"><span class="c0">informal: imprecise</span></li><li class="c7 c11 li-bullet-0"><span class="c0">formal: precise</span></li></ul><ul class="c3 lst-kix_kt1x3xteemmb-0"><li class="c6 li-bullet-0"><span class="c0">natural language specification</span></li></ul><ul class="c3 lst-kix_kt1x3xteemmb-1 start"><li class="c7 c11 li-bullet-0"><span class="c0">informal</span></li><li class="c7 c11 li-bullet-0"><span class="c0">can be more readable than a mathematical specification, but…</span></li><li class="c7 c11 li-bullet-0"><span class="c0">you must deal with things like verbosity, ambiguity, contradictions, etc.</span></li><li class="c7 c11 li-bullet-0"><span class="c0">it is much easier to people to misinterpret them</span></li></ul><ul class="c3 lst-kix_kt1x3xteemmb-0"><li class="c6 li-bullet-0"><span class="c0">mathematical specification</span></li></ul><ul class="c3 lst-kix_kt1x3xteemmb-1 start"><li class="c7 c11 li-bullet-0"><span class="c0">formal</span></li><li class="c7 c11 li-bullet-0"><span class="c0">the syntax can vary, but usually in the form of a purpose-built logic language based on the grammar of propositional logic</span></li></ul><h1 class="c2" id="h.eqiq0zs5ctk8"><span class="c14">Evidence</span></h1><ul class="c3 lst-kix_dg4znuy70dl9-0 start"><li class="c6 li-bullet-0"><span class="c0">benefits of restricted prescriptive grammar</span></li></ul><ul class="c3 lst-kix_dg4znuy70dl9-1 start"><li class="c7 c11 li-bullet-0"><span class="c0">computers can parse the specification language, enabling certain benefits</span></li><li class="c7 c11 li-bullet-0"><span class="c0">issues like ambiguity can be avoided, as keywords will have specified singular meanings</span></li></ul><ul class="c3 lst-kix_dg4znuy70dl9-0"><li class="c6 li-bullet-0"><span class="c0">benefits of human readability</span></li></ul><ul class="c3 lst-kix_dg4znuy70dl9-1 start"><li class="c7 c11 li-bullet-0"><span class="c0">because specifications are written in natural language, anyone can parse them to know they’re correct, including users, QAs, executives, designers, and anyone else who may lack technical expertise</span></li><li class="c7 c11 li-bullet-0"><span class="c0">we process code differently from natural language (Ivanova et al., 2020)</span></li></ul><ul class="c3 lst-kix_dg4znuy70dl9-2 start"><li class="c7 c13 li-bullet-0"><span class="c0">reading code makes minimal to no use of the language system, while code rephrased into a natural language problem does</span></li><li class="c7 c13 li-bullet-0"><span class="c0">having a natural language description of a problem may make it easier for people with less CS experience to understand</span></li></ul><ul class="c3 lst-kix_dg4znuy70dl9-0"><li class="c6 li-bullet-0"><span class="c0">benefits of computer readability</span></li></ul><ul class="c3 lst-kix_dg4znuy70dl9-1 start"><li class="c7 c11 li-bullet-0"><span class="c0">specifications can be automatically validated and implementations verified</span></li></ul><ul class="c3 lst-kix_dg4znuy70dl9-2 start"><li class="c7 c13 li-bullet-0"><span class="c0">this avoids issues like drift, contradictions</span></li></ul><ul class="c3 lst-kix_dg4znuy70dl9-1"><li class="c7 c11 li-bullet-0"><span class="c0">specifications can emit code</span></li></ul><ul class="c3 lst-kix_dg4znuy70dl9-2 start"><li class="c7 c13 li-bullet-0"><span class="c0">allows specifications to be checked for logic errors, run by users before properly implemented</span></li><li class="c7 c13 li-bullet-0"><span class="c0">can also act as a template for an implementation</span></li></ul><ul class="c3 lst-kix_dg4znuy70dl9-0"><li class="c6 li-bullet-0"><span class="c0">let’s imagine an implementation</span></li></ul><ul class="c3 lst-kix_dg4znuy70dl9-1 start"><li class="c7 c11 li-bullet-0"><span>we will use the work of the </span><span class="c16"><a class="c18" href="https://www.google.com/url?q=https://whatwg.org/faq&sa=D&source=editors&ust=1691984934406022&usg=AOvVaw0dEFkRDgnHRXk5TCSJWwqS">WHATWG</a></span><span class="c0"> as a base</span></li></ul><ul class="c3 lst-kix_dg4znuy70dl9-2 start"><li class="c7 c13 li-bullet-0"><span class="c0">the Web Hypertext Application Technology Working Group is an engineering group that writes specifications for web browsers and associated technologies</span></li><li class="c7 c13 li-bullet-0"><span>their specifications, or </span><span class="c9">standards</span><span>, use a custom natural language specification grammar as defined in their </span><span class="c16"><a class="c18" href="https://www.google.com/url?q=https://infra.spec.whatwg.org/%23algorithms&sa=D&source=editors&ust=1691984934406460&usg=AOvVaw2e0J80YLCT3HuX_LfnWID7">“Infra Standard”</a></span></li><li class="c7 c13 li-bullet-0"><span>that grammar is then encased in a lightweight extension of the HyperText Markup Language called </span><span class="c16"><a class="c18" href="https://www.google.com/url?q=https://speced.github.io/bikeshed/&sa=D&source=editors&ust=1691984934406783&usg=AOvVaw3udIiPwCxb9hsmwDKK4TvU">Bikeshed</a></span></li></ul><ul class="c3 lst-kix_dg4znuy70dl9-1"><li class="c7 c11 li-bullet-0"><span class="c0">by default, the written is not interpreted as code; this is good for describing the purpose of the specification and sharing prior art</span></li><li class="c7 c11 li-bullet-0"><span class="c0">definitions, marked by the use of the <dfn> tag, are used to declare types and constraints</span></li><li class="c7 c11 li-bullet-0"><span class="c0">algorithms, analogous to functions, are re-usable series of steps that do stuff</span></li><li class="c7 c11 li-bullet-0"><span class="c0">definitions and algorithms implemented in one specification can be referenced in another hence why types defined in the Infra Standard can be used in other WHATWG Standards</span></li><li class="c7 c11 li-bullet-0"><span class="c0">using prescriptive grammar to remove ambiguity</span></li></ul><ul class="c3 lst-kix_dg4znuy70dl9-2 start"><li class="c7 c13 li-bullet-0"><span class="c26">The word "or", in cases where both inclusive "or" and exclusive "or" are possible (e.g., "if either width or height is zero"), means an inclusive "or" (implying "or both"), unless it is called out as being exclusive (with "but not both").</span><span> (</span><span class="c16"><a class="c18" href="https://www.google.com/url?q=https://infra.spec.whatwg.org/%23terminology&sa=D&source=editors&ust=1691984934407452&usg=AOvVaw2uKhqoy6q2Rx8X6XPETo21">Infra</a></span><span class="c0">)</span></li><li class="c7 c13 li-bullet-0"><span class="c0">“or” has a clearly defined meaning</span></li></ul><ul class="c3 lst-kix_dg4znuy70dl9-1"><li class="c7 c11 li-bullet-0"><span class="c0">using restrictive grammar to remove ambiguity</span></li></ul><ul class="c3 lst-kix_dg4znuy70dl9-2 start"><li class="c7 c13 li-bullet-0"><span class="c26">The keywords "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "NOT RECOMMENDED", "MAY", and "OPTIONAL" are to be interpreted as described in RFC 2119.These keywords have equivalent meaning when written in lowercase and cannot appear in non-normative content.</span><span> (</span><span class="c16"><a class="c18" href="https://www.google.com/url?q=https://infra.spec.whatwg.org/%23conformance&sa=D&source=editors&ust=1691984934408049&usg=AOvVaw35LMQK8dtIaFYz3K-cKndq">Infra</a></span><span class="c0">)</span></li></ul><ul class="c3 lst-kix_dg4znuy70dl9-1"><li class="c7 c11 li-bullet-0"><span class="c0">leaning on natural language syntax</span></li></ul><ul class="c3 lst-kix_dg4znuy70dl9-2 start"><li class="c7 c13 li-bullet-0"><span class="c29">Algorithm names are usually verb phrases, but sometimes are given names that emphasize their standalone existence, so that standards and readers can refer to the algorithm more idiomatically. … (For non-verb phrase algorithm names, use "To perform the </span><span class="c4 c29">[algorithm name]</span><span class="c29">…")</span><span> (</span><span class="c16"><a class="c18" href="https://www.google.com/url?q=https://infra.spec.whatwg.org/%23algorithm-declaration&sa=D&source=editors&ust=1691984934408644&usg=AOvVaw0euPVmxbnMqjqvDXwN-_aq">Infra</a></span><span class="c0">)</span></li></ul><ul class="c3 lst-kix_dg4znuy70dl9-1"><li class="c7 c11 li-bullet-0"><span class="c0">notes to self</span></li></ul><ul class="c3 lst-kix_dg4znuy70dl9-2 start"><li class="c7 c13 li-bullet-0"><span class="c0">I only have 20 minutes and exploring limitations and implications, I feel, are more important for my general audience than implementation, so don’t go in too deep.</span></li><li class="c7 c13 li-bullet-0"><span class="c0">Rely on the audience’s existing understanding of syntax without introducing too many linguistics concepts; we’re already introducing a lot of CS/engineering stuff.</span></li></ul><h1 class="c2" id="h.v72zdecxn5v"><span class="c14">Limitations</span></h1><ul class="c3 lst-kix_bwcnx74ykyp6-0"><li class="c6 li-bullet-0"><span class="c0">resolving the “seven sins” of existing natural language specifications (Meyer, 1985)</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-1 start"><li class="c7 c11 li-bullet-0"><span class="c0">noise</span></li><li class="c7 c11 li-bullet-0"><span class="c0">silence</span></li><li class="c7 c11 li-bullet-0"><span class="c0">over-specification</span></li><li class="c7 c11 li-bullet-0"><span class="c0">contradiction</span></li><li class="c7 c11 li-bullet-0"><span class="c0">ambiguity</span></li><li class="c7 c11 li-bullet-0"><span class="c0">forward reference</span></li><li class="c7 c11 li-bullet-0"><span class="c0">wishful thinking</span></li><li class="c7 c11 li-bullet-0"><span class="c0">Meyer also suggests that formal specifications can act as a base for writing a stronger natural language specification, but issues like drift will naturally take place if one is to maintain two specifications.</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-0"><li class="c6 li-bullet-0"><span class="c0">resolving qualms with executable specifications (Hayes & Jones, 1989; Fuchs, 1992)</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-1 start"><li class="c7 c11 li-bullet-0"><span class="c0">executable specifications are too restrictive</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-2 start"><li class="c7 c13 li-bullet-0"><span class="c0">argued against by Fuchs with example specifications in his paper</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-1"><li class="c7 c11 li-bullet-0"><span class="c0">semi-concrete specifications are hard to implement</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-2 start"><li class="c7 c13 li-bullet-0"><span class="c0">specifications can generate as much code as possible and let implementors fill in the gaps</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-1"><li class="c7 c11 li-bullet-0"><span class="c0">keeping specification and prototyping separate</span></li></ul><ul class="c3 lst-kix_bwcnx74ykyp6-2 start"><li class="c7 c13 li-bullet-0"><span>I think blurring the lines a little may have a lot of benefits, especially since some dev teams hit the ground running with a prototype and then return later to write a spec; prototyping in an executable spec lang would allow a development workflow like that to naturally take place</span></li></ul></body></html>