Skip to content

Remove import <decreases/*.vpr> #24

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

Remove import <decreases/*.vpr> #24

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
19 changes: 1 addition & 18 deletions tutorial/termination.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,6 @@ Here, `<tuple>` denotes the termination measure: a tuple of comma-separated expr
A common example for termination is the standard `factorial` function, which terminates because its argument decreases with respect to the usual well-founded order over non-negative numbers.

```silver-runnable
import <decreases/int.vpr>

function factorial(n:Int) : Int
requires 0 <= n
decreases n
Expand All @@ -37,7 +35,7 @@ Viper successfully verifies that `factorial` terminates: at each recursive invoc

### Predefined Well-Founded Orders {#term_prov_wfo}

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.
Viper's standard library provides definitions of well-founded orders for most types built into Viper. They are automatically imported upon use of a `decreases` statement. Alternatively, they can also 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 |
| ---- | ---- |
Expand All @@ -56,8 +54,6 @@ All definitions are straightforward, except the last one, which is concerned wit
Viper uses this nesting relation to enable termination checks based on predicate instances, as illustrated by the next example, the recursive computation of the length of a linked list: intuitively, the remainder of the linked list, represented by predicate instance `list(this)`, is used as the termination measure. This works because the recursive call is nested under the unfolding of `list(this)`, and takes the smaller predicate instance `list(this.next)`.

```silver-runnable
import <decreases/predicate_instance.vpr>

field next: Ref

predicate list(this: Ref) {
Expand Down Expand Up @@ -100,8 +96,6 @@ Special cases, such as empty tuples, tuples of different length, and tuples of d
A typical example of a function for which a tuple as termination measure is used, is the Ackermann function:

```silver-runnable
import <decreases/int.vpr>

function ack(m:Int, n:Int):Int
decreases m, n
requires m >= 0
Expand Down Expand Up @@ -189,8 +183,6 @@ As previously mentioned, Viper offers [predefined orders](#term_prov_wfo) for it
In the remainder of this subsection, both approaches will be illustrated using a combination of the `MyInt` example (from the earlier subsection on domains) and a `factorial` function operating on `MyInt`. In the example below, the destructor `get` is used to map a `MyInt` to a regular `Int`, which indirectly allows using `MyInt` in the function's decreases clause.

```silver-runnable
import <decreases/int.vpr>

domain MyInt {
function put(i: Int): MyInt // Constructor
function get(m: MyInt): Int // Destructor
Expand Down Expand Up @@ -257,8 +249,6 @@ For mutually recursive functions, Viper implements the following approach (as, e
A simple case of mutual recursion is illustrated next, by functions `is_even` and `is_odd`:

```silver-runnable
import <decreases/int.vpr>

function is_even(x: Int): Bool
requires x >= 0
decreases x
Expand All @@ -279,9 +269,6 @@ Consider function `is_even`: its termination measure `x` decreases at the indire
In the example above, the two termination measures are tuples of equal length and type. However, this is not required of mutually recursive functions in order to prove their termination. Consider the next example (which verifies successfully):

```silver-runnable
import <decreases/int.vpr>
import <decreases/bool.vpr>

function fun1(y: Int, b: Bool): Int
decreases y, b
{
Expand Down Expand Up @@ -326,8 +313,6 @@ To ensure soundness, only a *single* clause per kind of measure is allowed. More
The following example illustrates combined conditional termination clauses: function `sign` promises to decrease `x` if positive, and something (wildcard) if `x` is negative. In case `x` is zero, function `sign` does not (promise to) terminate.

```silver-runnable
import <decreases/int.vpr>

function sign(x: Int): Int
decreases x if 1 <= x
decreases _ if x <= -1
Expand Down Expand Up @@ -431,8 +416,6 @@ The currently implemented approach to checking termination of methods is similar
A straightforward example is method `sum`, shown next:

```silver-runnable
import <decreases/int.vpr>

method sum(n: Int) returns (res: Int)
requires 0 <= n
decreases
Expand Down