Skip to content

Fix typos #23

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
fosslinux wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Fix typos #23

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions tutorial/structure.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,7 @@ domain Pair[A, B] {
* Declared by keyword `domain`
* Have a name, which is introduced as an additional _type_ in the Viper program
* Domains may have type parameters (e.g. `A` and `B` above)
* A domain's body (delimited by braces) consists of a number function declarations, followed by a number of axioms
* A domain's body (delimited by braces) consists of a number of function declarations, followed by a number of axioms
* Domain functions (functions declared inside a `domain`) may have neither a body nor a specification; these are uninterpreted total mathematical functions
* Domain axioms consist of name (following the `axiom` keyword), and a definition enclosed within braces (which is a boolean expression which may not read the program state in any way)
* Useful for specifying custom mathematical theories
Expand All @@ -119,7 +119,7 @@ define link(x, y) {
* Macros are not type-checked until after expansion
* However, macro bodies must be well-formed assertions / statements
* May have any number of (untyped) parameter names (e.g. `a` and `b` above)
* The are two kinds of macros
* There are two kinds of macros
* Macros defining assertions (or expressions) include the macro definition whitespace-separated afterwards (e.g. `plus` above)
* Macros defining _statements_ include their definitions within braces (e.g. `link` above)
* See the [array domain encoding](#array-domain) for an example
Expand Down
2 changes: 1 addition & 1 deletion tutorial/termination.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ Viper successfully verifies that `factorial` terminates: at each recursive invoc

Viper's standard library provides definitions of well-founded orders for most types built into Viper, all of which can be imported from the `decreases` folder. The following table lists all provided orders; we write `s1 <_ s2` if `s1` is less than `s2` with respect to the order.

| Build-In Type<br>(file name) | Provided Well-Founded Order |
| Built-In Type<br>(file name) | Provided Well-Founded Order |
| ---- | ---- |
|`Ref`<br>(`ref.vpr`)| `r1 <_ r2 <==> r1 == null && r2 != null`
|`Bool`<br>(`bool.vpr`)| `b1 <_ b2 <==> b1 == false && b2 == true`
Expand Down