===============
The most effective way to get bugs out of code is code review. More than running the code, more than unit tests, having someone else review an author's code is the best technique known to eliminate bugs (Fagan 1975 and Cohen 2006).
Jay Parlar parlarjb
parlarjb
/ resources.als
Created
August 27, 2019 02:21
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| one sig Person { | |
| } | |
| sig Resource { | |
| , access: set Person | |
| , parent: lone Resource | |
| } | |
| fact "No cycles" { |
parlarjb
/ accounts.als
Created
August 30, 2019 01:34
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| sig Account { | |
| resources: set Resource, | |
| users: set User | |
| } | |
| sig User { | |
| canAccess: some Resource | |
| } | |
| sig Resource { |
parlarjb
/ codereview.md
Last active
December 18, 2024 22:39
parlarjb
/ startrek.py
Created
September 25, 2019 17:14
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| from z3 import * | |
| s = Solver() | |
| Name, name_consts = EnumSort("Name", | |
| ["Riker", "Beverly", "Data", "Troi"]) | |
| riker, beverly, data, troi = name_consts | |
| Planet, planet_consts = EnumSort("Planet", | |
| ["Betazed", "Dytallix B", "Risa", "Tellar"]) |
parlarjb
/ startrek.py
Created
September 25, 2019 17:14
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| from z3 import * | |
| s = Solver() | |
| Name, name_consts = EnumSort("Name", | |
| ["Riker", "Beverly", "Data", "Troi"]) | |
| riker, beverly, data, troi = name_consts | |
| Planet, planet_consts = EnumSort("Planet", | |
| ["Betazed", "Dytallix B", "Risa", "Tellar"]) |
parlarjb
/ startrek.py
Last active
September 25, 2019 17:52
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| from z3 import * | |
| s = Solver() | |
| Name, name_consts = EnumSort("Name", | |
| ["Riker", "Beverly", "Data", "Troi"]) | |
| riker, beverly, data, troi = name_consts | |
| Planet, planet_consts = EnumSort("Planet", | |
| ["Betazed", "Dytallix B", "Risa", "Tellar"]) |
parlarjb
/ prbuddies.py
Last active
February 29, 2020 22:27
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| from z3 import * | |
| import itertools | |
| s = Solver() | |
| names = ['Ali', 'Kelsey', 'Yuan', 'Chris', 'Narges', 'Weija', 'Jay', 'Linh', 'Joseph', 'Lucy'] | |
| nmap = {} # Maps string name to integer value | |
| imap = {} # Reverse map, integer value to string name | |
| for i, name in enumerate(names): | |
| nmap[name] = i |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| open util/ordering[Time] | |
| sig Time {} | |
| sig Key { | |
| pressed: set Time | |
| } | |
| abstract sig Event { | |
| pre, post: Time, | |
| key: Key |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Analyzing programs with Z3: https://www.youtube.com/watch?v=ruNFcH-KibY | |
| Software Synthesis via sketching thesis http://people.csail.mit.edu/asolar/papers/thesis.pdf | |
| ericpony.github.io/z3py-tutorial/guide-examples.htm | |
| http://ericpony.github.io/z3py-tutorial/advanced-examples.htm | |
| https://theory.stanford.edu/~nikolaj/programmingz3.html | |
| A big tutorial: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.225.8231&rep=rep1&type=pdf | |
| http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.367.9961&rep=rep1&type=pdf |
OlderNewer