Flow dependency contracts

There is a small number (two or three) of simple features (mostly derived from Ada language) I'd like to see in a modern system language, but I don't know if they are useful and good for Rust, and if they are worth implementing and having. Here I'll explain one of them.

In languages like C, Object Pascal (Dephi / FreePascal), C++, D, Python, and several others, I have had several small bugs in my code caused by using by mistake module-level (or global-level) variables instead of function-local variables, or local ones instead of module ones. They are problems caused by using variable names from the wrong scope. Thankfully those bugs didn't cause me large problems, but I prefer to avoid bugs when it's reasonably easy and handy to do so.

In D language I reduce this problem annotating functions with "pure" as often as possible. This forbids the function to access module-level mutables, so only module-level enums/consts/immutables can be used (and I also sometimes prefix instance variables with "this." to avoid some bugs caused by confusing local variables with instance variables). Some C++ programmers prefix global variables with "g_".

In Rust this problem is reduced because in struct impls you need to prefix the instance variables with "self." (as in Python. While in D and other languages you aren't required to use "this."), so there's less risk of mixing the scope of variables. And in safe Rust code you can't access module-level mutables. So Rust functions are "partially pure" by default. On the other hand module-level mutables are sometimes handy, and Rust allows them in unsafe contexts/functions:

static mut X: u32 = 0;
fn main() {
    unsafe {
        X += 1;
    }
}

The feature I discuss in this post allows to manage the global (module-level) mutable state, to avoid some of the bugs I have hit in past years. It's derived from a Ada/SPARK language feature, and it's easy to understand and use. Compared to languages like D, this feature is less useful for Rust because accessing global mutables is probably rare in Rust. But if you use global mutables in Rust code, this feature could be useful to you. This feature is used in Ada/SPARK code also to allow the static verification of the procedures (void functions), and this could be useful in Rust too, to write high-integrity Rust code in future, and replace some usages of Ada with Rust in satellites, critical control systems in industry, safety critical aviation or medicine systems, and so on. It's a small software niche, but sufficiently important. And writing high integrity code in Rust (or a Rust subset) sounds better than doing it in MISRA-C :slight_smile:

In Ada/SPARK you can write code like:

procedure Draw_Line(A, B: in Point)
  with
    Global => (Input => Line_Algorithm,
               Output => (Status, Error),
               In_Out => Line_Count);

The Draw_Line is a procedure so it returns nothing (void in C), but it accesses some global variables (and it takes the A and B input arguments). So SPARK requires you to write an annotation inside the function that tells what global variables are read, written, and read & written by the procedure (this is the basic usage, there are other refinements, that allow to write a hierarchy of such annotations, to write such annotations for modules too, and some syntax sugar to shorten the annotation in standard situations. More details and refinements can be found in the book "Building High Integrity Applications with SPARK" by McCormick and Chapin). The compiler verifies statically that the annotation is strictly correct (it has zero run-time overhead).

Such annotations help avoid my bugs of using variables from the wrong scope, document exactly where variables come from (and it's "documentation" that can't go out of sync with the code), and allow verification of the code:

The SPARK tools will understand that, because the global variable has an input mode, it must be initialized in some way before Draw_Line can be called.

You can imagine an equivalent optional Rust annotation like:

#[globals(in line_algorithm, out status, out error, inout line_count)]
fn draw_line(a: Point, b: Point) {...}

Where "in" means draw_line() just reads that global variable, "out" means it just writes it, and "inout" means it reads and writes that global variable.

In Rust you can also nest functions (I do it often), so you could also support a more general annotation:

#[outer(in line_algorithm, out status, out error, inout line_count)]
fn draw_line(a: Point, b: Point) {...}

Where "outer" means the scope just outside the function draw_line(). This allows inner functions to use variables from the function that encloses it.

An annotation like #[outer()] means the function doesn't read/write mutables from outer scopes (it doesn't mean the function is pure. I/O is still allowed).

For high-integrity Rust code you can even think having a simple extra annotation that requires all module-level functions to have a flow dependency contract, something like:

#![require(flow_dependency_contracts)]

2 Likes

This seems more like a closure where you explicitly specify the bindings it does (like in c++ lambdas)


Ada uses packages (modules) to emulate singletons (due to missing the ownership concept). Rust rarely needs global statics. Most of the time you can get the same effect by creating an object and calling the functions on that object. I don't see the additional value this brings us, I'd even say this encourages the abuse of global statics.

1 Like

I recently thought about how I could achieve this without requiring any change in rustic. Iā€™d write a lint that stores

  • inherent mutability and contents for all type items
  • all calls within a function item (and possibly whether those calls are conditional)

This would let us know purity, panicking, infinite loops by recursion, etc. without stopping at the crate boundary.

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.