Skip to content

Commit c8e91a5

Browse files
willyrosssmoelius
authored andcommitted
Fix README typo in the Possible theoretical foundation section
1 parent 16d582c commit c8e91a5

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

README.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -128,7 +128,7 @@ Now, imagine we were to apply this procedure, and consider a statement `S` that
128128

129129
**Case 2**: `S`'s precondition is stronger than its postcondition (e.g., `S` is an assertion). Then `S` imposes constraints on the environments in which it executes. Put another way, `S` _tests_ something. Thus, removing `S` would likely detract from the test's overarching purpose.
130130

131-
Conversely, consider a statement `S` that satisfies (`*`). Here is why it might make sense to remove `S`. Think of `S` as _shifting_ the set of valid environments, rather than constraining them. More precisely, if `S`'s weakest precondition `P` does not imply `Q`, and if `Q` is satisfiable, the there is an assignment to `P` and `Q`'s free variables that satisfies both `P` and `Q`. If such an assignment results from each environment in which `S` is actually executed, then the necessity of `S` is called into question.
131+
Conversely, consider a statement `S` that satisfies (`*`). Here is why it might make sense to remove `S`. Think of `S` as _shifting_ the set of valid environments, rather than constraining them. More precisely, if `S`'s weakest precondition `P` does not imply `Q`, and if `Q` is satisfiable, then there is an assignment to `P` and `Q`'s free variables that satisfies both `P` and `Q`. If such an assignment results from each environment in which `S` is actually executed, then the necessity of `S` is called into question.
132132

133133
The main utility of (`*`) is in helping to select the functions, macros, and method calls that Necessist ignores. Necessist ignores certain of these by default. Suppose that, for one of the frameworks, we are considering whether Necessist should ignore some function `foo`. If we imagine a predicate transformer semantics for the framework's testing language, we can ask: if statement `S` were a call to `foo`, would `S` satisfy (`*`)? If the answer is "no," then Necessist should likely ignore `foo`.
134134

0 commit comments

Comments
 (0)