Create dedicated top-level pre-post-conditions article

docs/anti-patterns.md

@@ -1,6 +1,6 @@
 ---
 title: Cadence Anti-Patterns
-sidebar_position: 6
+sidebar_position: 8
 sidebar_label: Anti-Patterns
 ---
 

docs/cadence-migration-guide/_category_.json

@@ -1,3 +1,3 @@
 {
-    "position": 5
+    "position": 6
 }

docs/contract-upgrades.md

@@ -1,5 +1,6 @@
 ---
 title: Contract Upgrades with Incompatible Changes
+sidebar_position: 11
 ---
 
 ### Problem

docs/design-patterns.md

@@ -1,6 +1,6 @@
 ---
 title: Cadence Design Patterns
-sidebar_position: 5
+sidebar_position: 7
 sidebar_label: Design Patterns
 ---
 

docs/json-cadence-spec.md

@@ -1,6 +1,7 @@
 ---
 title: JSON-Cadence Data Interchange Format
-sidebar_label: JSON-Cadence format
+sidebar_label: JSON-Cadence Format
+sidebar_position: 12
 ---
 
 > Version 0.3.1

docs/language/_category_.json

@@ -1,3 +1,3 @@
 {
-    "position": 4
+    "position": 5
 }

docs/language/access-control.md

@@ -1,6 +1,6 @@
 ---
 title: Access control
-sidebar_position: 10
+sidebar_position: 11
 ---
 
 Access control allows making certain parts of a program accessible/visible

docs/language/accounts/_category_.json

@@ -1,3 +1,3 @@
 {
-    "position": 16
+    "position": 17
 }

docs/language/attachments.mdx

@@ -1,6 +1,6 @@
 ---
 title: Attachments
-sidebar_position: 17
+sidebar_position: 18
 ---
 
 Attachments are a feature of Cadence designed to allow developers to extend a struct or resource type

docs/language/built-in-functions.mdx

@@ -1,6 +1,6 @@
 ---
 title: Built-in Functions
-sidebar_position: 23
+sidebar_position: 24
 ---
 
 ## `panic`

docs/language/capabilities.md

@@ -1,6 +1,6 @@
 ---
 title: Capabilities
-sidebar_position: 11
+sidebar_position: 12
 ---
 
 Cadence supports [capability-based security](https://en.wikipedia.org/wiki/Capability-based_security)

docs/language/contract-updatability.md

@@ -1,6 +1,6 @@
 ---
 title: Contract Updatability
-sidebar_position: 19
+sidebar_position: 20
 ---
 
 ## Introduction

docs/language/contracts.mdx

@@ -1,6 +1,6 @@
 ---
 title: Contracts
-sidebar_position: 18
+sidebar_position: 19
 ---
 
 A contract is a collection of type definitions,

docs/language/control-flow.md

@@ -1,6 +1,6 @@
 ---
 title: Control Flow
-sidebar_position: 7
+sidebar_position: 8
 ---
 
 Control flow statements control the flow of execution in a function.

docs/language/core-events.md

@@ -1,6 +1,6 @@
 ---
 title: Core Events
-sidebar_position: 22
+sidebar_position: 23
 ---
 
 Core events are events emitted directly from the FVM (Flow Virtual Machine).

docs/language/crypto.mdx

@@ -1,6 +1,6 @@
 ---
 title: Crypto
-sidebar_position: 25
+sidebar_position: 26
 ---
 
 ## Hash algorithms

docs/language/enumerations.md

@@ -1,6 +1,6 @@
 ---
 title: Enumerations
-sidebar_position: 13
+sidebar_position: 14
 ---
 
 Enumerations are sets of symbolic names bound to unique, constant values,

docs/language/environment-information.md

@@ -1,6 +1,6 @@
 ---
 title: Environment Information
-sidebar_position: 24
+sidebar_position: 25
 ---
 
 ## Transaction Information

docs/language/events.md

@@ -1,6 +1,6 @@
 ---
 title: Events
-sidebar_position: 21
+sidebar_position: 22
 ---
 
 Events are special values that can be emitted during the execution of a program.

docs/language/functions.mdx

@@ -405,85 +405,9 @@ fun test(x: Int) {
 }
 ```
 
-## Function Preconditions and Postconditions
+## Function pre-conditions and post-conditions
 
-Functions may have preconditions and may have postconditions.
-Preconditions and postconditions can be used to restrict the inputs (values for parameters)
-and output (return value) of a function.
-
-Preconditions must be true right before the execution of the function.
-Preconditions are part of the function and introduced by the `pre` keyword,
-followed by the condition block.
-
-Postconditions must be true right after the execution of the function.
-Postconditions are part of the function and introduced by the `post` keyword,
-followed by the condition block.
-Postconditions may only occur after preconditions, if any.
-
-A conditions block consists of one or more conditions.
-Conditions are expressions evaluating to a boolean.
-
-Conditions may be written on separate lines,
-or multiple conditions can be written on the same line,
-separated by a semicolon.
-This syntax follows the syntax for [statements](./syntax.md#semicolons).
-
-Following each condition, an optional description can be provided after a colon.
-The condition description is used as an error message when the condition fails.
-
-In postconditions, the special constant `result` refers to the result of the function.
-
-```cadence
-fun factorial(_ n: Int): Int {
-    pre {
-        // Require the parameter `n` to be greater than or equal to zero.
-        //
-        n >= 0:
-            "factorial is only defined for integers greater than or equal to zero"
-    }
-    post {
-        // Ensure the result will be greater than or equal to 1.
-        //
-        result >= 1:
-            "the result must be greater than or equal to 1"
-    }
-
-    if n < 1 {
-       return 1
-    }
-
-    return n * factorial(n - 1)
-}
-
-factorial(5)  // is `120`
-
-// Run-time error: The given argument does not satisfy
-// the precondition `n >= 0` of the function, the program aborts.
-//
-factorial(-2)
-```
-
-In postconditions, the special function `before` can be used
-to get the value of an expression just before the function is called.
-
-```cadence
-var n = 0
-
-fun incrementN() {
-    post {
-        // Require the new value of `n` to be the old value of `n`, plus one.
-        //
-        n == before(n) + 1:
-            "n must be incremented by 1"
-    }
-
-    n = n + 1
-}
-```
-
-Both preconditions and postconditions are considered [`view` contexts](#view-functions); 
-any operations that are not legal in functions with `view` annotations are also not allowed in conditions. 
-In particular, this means that if you wish to call a function in a condition, that function must be `view`. 
+See [function pre-condition and post-condition] for more information.
 
 ## View Functions
 
@@ -617,3 +541,7 @@ let newIntegers = transform(function: double, integers: [1, 2, 3])
 // `newIntegers` is `[2, 4, 6]`
 ```
 
+<!-- Relative links. Will not render on the page -->
+
+[function pre-condition and post-condition]: ./pre-and-post-conditions.md#function-pre-conditions-and-post-conditions
+

docs/language/glossary.mdx

@@ -1,6 +1,6 @@
 ---
 title: Glossary
-sidebar_position: 26
+sidebar_position: 27
 ---
 
 

docs/language/imports.mdx

@@ -1,6 +1,6 @@
 ---
 title: Imports
-sidebar_position: 15
+sidebar_position: 16
 ---
 
 Programs can import declarations (types, functions, variables, etc.) from other programs.

docs/language/interfaces.mdx

@@ -1,6 +1,6 @@
 ---
 title: Interfaces
-sidebar_position: 12
+sidebar_position: 13
 ---
 
 An interface is an abstract type that specifies the behavior of types
@@ -48,113 +48,7 @@ some aspects of them will always hold.
 
 ## Interface Declaration
 
-Interfaces are declared using the `struct`, `resource`, or `contract` keyword,
-followed by the `interface` keyword,
-the name of the interface,
-and the requirements, which must be enclosed in opening and closing braces.
-
-Field requirements can be annotated to
-require the implementation to be a variable field, by using the `var` keyword;
-require the implementation to be a constant field, by using the `let` keyword;
-or the field requirement may specify nothing,
-in which case the implementation may either be a variable or a constant field.
-
-Field requirements and function requirements must specify the required level of access.
-The access must be at least be public, so the `access(all)` keyword must be provided.
-
-Interfaces can be used in types.
-This is explained in detail in the section [Interfaces in Types](#interfaces-in-types).
-For now, the syntax `{I}` can be read as the type of any value that implements the interface `I`.
-
-```cadence
-// Declare a resource interface for a fungible token.
-// Only resources can implement this resource interface.
-//
-access(all)
-resource interface FungibleToken {
-
-    // Require the implementing type to provide a field for the balance
-    // that is readable in all scopes (`access(all)`).
-    //
-    // Neither the `var` keyword, nor the `let` keyword is used,
-    // so the field may be implemented as either a variable
-    // or as a constant field.
-    //
-    access(all)
-    balance: Int
-
-    // Require the implementing type to provide an initializer that
-    // given the initial balance, must initialize the balance field.
-    //
-    init(balance: Int) {
-        pre {
-            balance >= 0:
-                "Balances are always non-negative"
-        }
-        post {
-            self.balance == balance:
-                "the balance must be initialized to the initial balance"
-        }
-
-        // NOTE: The declaration contains no implementation code.
-    }
-
-    // Require the implementing type to provide a function that is
-    // callable in all scopes, which withdraws an amount from
-    // this fungible token and returns the withdrawn amount as
-    // a new fungible token.
-    //
-    // The given amount must be positive and the function implementation
-    // must add the amount to the balance.
-    //
-    // The function must return a new fungible token.
-    // The type `{FungibleToken}` is the type of any resource
-    // that implements the resource interface `FungibleToken`.
-    //
-    access(all)
-    fun withdraw(amount: Int): @{FungibleToken} {
-        pre {
-            amount > 0:
-                "the amount must be positive"
-            amount <= self.balance:
-                "insufficient funds: the amount must be smaller or equal to the balance"
-        }
-        post {
-            self.balance == before(self.balance) - amount:
-                "the amount must be deducted from the balance"
-        }
-
-        // NOTE: The declaration contains no implementation code.
-    }
-
-    // Require the implementing type to provide a function that is
-    // callable in all scopes, which deposits a fungible token
-    // into this fungible token.
-    //
-    // No precondition is required to check the given token's balance
-    // is positive, as this condition is already ensured by
-    // the field requirement.
-    //
-    // The parameter type `{FungibleToken}` is the type of any resource
-    // that implements the resource interface `FungibleToken`.
-    //
-    access(all)
-    fun deposit(_ token: @{FungibleToken}) {
-        post {
-            self.balance == before(self.balance) + token.balance:
-                "the amount must be added to the balance"
-        }
-
-        // NOTE: The declaration contains no implementation code.
-    }
-}
-```
-
-Note that the required initializer and functions do not have any executable code.
-
-Struct and resource Interfaces can only be declared directly inside contracts,
-i.e. not inside of functions.
-Contract interfaces can only be declared globally and not inside contracts.
+See [interface declaration] for more information.
 
 ## Interface Implementation
 
@@ -1058,3 +952,7 @@ D
 B
 A
 ```
+
+<!-- Relative links. Will not render on the page -->
+
+[interface declaration]: ./pre-and-post-conditions.md#interface-declaration