Skip to content

Commit

Permalink
Update incorrect contract examples.
Browse files Browse the repository at this point in the history
  • Loading branch information
lerno committed Jul 30, 2024
1 parent e91e1e9 commit ef402e8
Showing 1 changed file with 32 additions and 24 deletions.
56 changes: 32 additions & 24 deletions src/content/docs/references/docs/contracts.md
Original file line number Diff line number Diff line change
Expand Up @@ -59,23 +59,23 @@ pointers may both be read from and written to without checks.
However, it should be noted that the compiler might not detect whether the annotation is correct or not! This program might compile, but will behave strangely:

```
fn void badFunc(int* i)
fn void bad_func(int* i)
{
*i = 2;
}
/**
* @param [in] i
*/
fn void lyingFunc(int* i)
fn void lying_func(int* i)
{
badFunc(i); // The compiler might not check this!
bad_func(i); // The compiler might not check this!
}
fn void test()
{
int a = 1;
lyingFunc(&a);
lying_func(&a);
io::printf("%d", a); // Might print 1!
}
```
Expand All @@ -86,63 +86,71 @@ However, compilers will usually detect this:
/**
* @param [in] i
*/
fn void badFunc(int* i)
fn void bad_func(int* i)
{
*i = 2; // <- Compiler error: cannot write to "in" parameter
}
```

### Pure in detail

The `pure` annotation allows a program to make assumptions in regard to how the function treats global variables. Unlike for `const`, a pure function is not allowed to call a function which is known to be impure.
The `pure` annotation allows a program to make assumptions in regard to how the function treats global variables.
Unlike for `const`, a pure function is not allowed to call a function which is known to be impure.

However, just like for `const` the compiler might not detect whether the annotation is correct or not! This program might compile, but will behave strangely:
However, just like for `const` the compiler might not detect whether the annotation
is correct or not! This program might compile, but will behave strangely:

```
```c3
int i = 0;
type Secretfn fn void();
def SecretFn = fn void();
fn void badFunc()
fn void bad_func()
{
i = 2;
}
Secretfn foo = nil;
/**
* @pure
*/
fn void lyingFunc()
fn void lying_func(SecretFn f)
{
SecretFunc(); // The compiler cannot reason about this!
f(); // The compiler cannot reason about this!
}
fn void test()
fn void main()
{
foo = &badFunc;
i = 1;
lyingFunc();
io::printf("%d", a); // Might print 1!
lying_func(&bad_func);
io::printf("%d", i); // Might print 1!
}
```

However, compilers will usually detect this:

```
```c3
int i = 0;
fn void badFunc()
def SecretFn = fn void();
fn void bad_func()
{
i = 2;
}
/**
* @pure
*/
fn void lyingFunc()
fn void lying_func(SecretFn f)
{
badFunc(); // Error! Calling an impure function
f(); // <- ERROR: Only '@pure' functions may be called.
}
fn void main()
{
i = 1;
lying_func(&bad_func);
io::printf("%d", i); // Might print 1!
}
```

Expand All @@ -155,13 +163,13 @@ In order to check macros, it's often useful to use the builtin `$defined`
function which returns true if the code inside would pass semantic checking.


```
```c3
/**
* @require $and($defined(resource.open), $defined(resource.open()) `Expected resource to have an "open" function`
* @require resource != nil
* @require $assignable(resource.open(), void*)
**/
macro openResource(resource)
macro open_resource(resource)
{
return resource.open();
}
Expand Down

0 comments on commit ef402e8

Please sign in to comment.