Struct Tokens 

pub struct Tokens<'a>(/* private fields */);

Invariant tokens.

This is given at the start of the program, and must be passed along to LocalInvariant::open to prevent opening invariant reentrantly.

Tokens and open

Tokens are used to avoid reentrency in open. To ensure this, Tokens acts as a special kind of mutable borrow : only one may exist at a given point in the program, preventing multiple calls to open with the same namespace. This is the reason this type has a lifetime attached to it.

Note that after the execution of open, the token that was used is restored. Because of this, we never need to talk about the ‘final’ value of this borrow, because it never differs from the current value (in places where we can use it).

To help passing it into functions, it may be reborrowed, similarly to a normal borrow.

Implementations

impl Tokens<'_>

pub fn namespaces(self) -> Set<Namespace>

Get the underlying set of namespaces of this token.

Also accessible via the view (@) operator.

(opaque)

pub fn new() -> Ghost<Self>

Get the tokens for all the namespaces.

This is only callable once, in main.

ensures

forall<ns: Namespace> result.contains(ns)

terminates

ghost

pub fn reborrow<'a>(&'a mut self) -> Tokens<'a>

Reborrow the token, allowing it to be reused later.

Example

fn foo(tokens: Ghost<Tokens>) {}
fn bar(tokens: Ghost<Tokens>) {}
fn baz(mut tokens: Ghost<Tokens>) {
    foo(ghost!(tokens.reborrow()));
    bar(tokens);
}

ensures

result == *self && ^self == *self

terminates

ghost

pub fn split<'a>( &'a mut self, ns: Snapshot<Namespace>, ) -> (Tokens<'a>, Tokens<'a>)

Split the tokens in two, so that it can be used to access independant invariants.

Example

declare_namespace! { FOO }
declare_namespace! { BAR }

// the lifetime 'locks' the namespace
#[requires(tokens.contains(FOO()))]
fn foo<'a>(tokens: Ghost<Tokens<'a>>) -> &'a i32 {
    // access some invariant to get the reference
}
#[requires(tokens.contains(BAR()))]
fn bar(tokens: Ghost<Tokens>) {}

#[requires(tokens.contains(FOO()) && tokens.contains(BAR()))]
fn baz(mut tokens: Ghost<Tokens>) -> i32 {
     let (ns_foo, ns_bar) = ghost!(tokens.split(snapshot!(FOO()))).split();
     let x = foo(ns_foo);
     bar(ns_bar);
     *x
}

requires

self.contains(*ns)

ensures

^self == *self

ensures

result.0.contains(*ns)

ensures

result.1.namespaces() == self.namespaces().remove(*ns)

terminates

ghost

pub fn contains(self, namespace: Namespace) -> bool

(open)

self.namespaces().contains(namespace)

Trait Implementations

impl View for Tokens<'_>

fn view(self) -> Set<Namespace>

(open, inline)

self.namespaces()

type ViewTy = Set<Namespace>