Static Assert

StaticAssert is something of the StaticTyping version of DesignByContract. As with StaticTyping, use of StaticAssert also allows the compiler to ProveAssumptions that keep the code very efficient. It significantly extends the abilities of the relatively 'dumb' type checkers aimed at StaticTypeSafety... though, by corollary, it requires that the language implementer greatly extend the abilities of these same 'dumb' type checkers.

In many ways, StaticAssert is equivalent to DependentTyping in a statically TypeSafe language. Accordingly, one must generally give up the property of 'guaranteed termination' in the TypeSafety checking. In practice, such features are implemented in AutomaticTheoremProving? or ProofAssistant? environments where explicit ProofOfCorrectness can be supplied, so this is not likely to be an issue. Additionally, a good IntegratedDevelopmentEnvironment can support TuringComplete typecheck phases by issuing warnings around the problem areas (so programmers can clean them up later) and also have a tuneable 'fail' timer to stop typechecking in error.

A language that provides SoftTyping might still provide StaticAssert, but would do well to also support 'soft' assertions wherever one normally sees an 'assert' statement - i.e. qualifying such an assertion as an 'error' only if it can be proven to fail, and removing the assertion from the runtime if it can be proven to pass, otherwise leaving it in (and optionally issuing a warning) when one 'cannot prove' either consequence.

In TypeTheory, the counterpart of StaticAssert is RefinementType? (see ProgramRefinement?). A RefinementType? of the form {x: A | P} denotes all elements of type A which also satisfy predicate P. Operationally, it is a (dependently typed) record containing x plus a proof that P holds for x.

---

Can we have some examples, please? Thanks!

Sure. Consider a typical operation with three conditions:

 Collection Collection::get_range(int start, int end) {
    static_assert(start <= end);
    static_assert(start >= 0);
    static_assert(end < size());

    Collection result;
    for( ; end != start; ++start) 
      result.push_back(this->at(start));
    return result;
  }

In code lacking static_assert, you could use DesignByContract principles and include a regular assertion or throw exceptions in order to get something of a RunTime safety. This costs you three comparisons every time you run the check (which is utterly trivial in this didactic case, but might be more significant in a O(1) function). Alternatively, you can just assume these three conditions are true, not check them, and thus save a little bit of time on the call (albeit not much in this case) and get UndefinedBehavior when you ask for 'this->at(-10)'.

With static_assert, however, it would be up to the compiler to prove that the conditions are met. Sometimes this would be really easy:

  myCollection.get_range(-10,11);  /// compiler error! violates condition 'start >= 0'.

Sometimes it would be a bit more difficult:

  int sum_range(Collection& c, int range_start, int range_end) {
    // inefficient didactic example...
    int result = 0;
    foreach item in c.get_range(range_start,range_end)
      result += item;
  }

  int main(args) {
    Collection c = collection_from_file("myCollection");
    int range_start = get_start(args);
    int range_end   = get_end(args);
    int result = sum_range(c,range_start,range_end); /// compiler error! cannot prove range_start <= range_end!
                                                     /// compiler error! cannot prove range_start >= 0
                                                     /// compiler error! cannot prove range_end < c.size()
    print(result);   
    return 0;
  }

Of course, the compiler error may be better or worse than that (emitting good compiler errors associated with TypeSafety is really difficult, and static_assert requires errors similar to those seen in DependentTyping).

In any case, you could fix this by putting some assertions or checks in prior. Static assert, like DependentTyping, can be program-path dependent.

  int main(args) {
    Collection c = collection_from_file("myCollection");
    int range_start = get_start(args);
    int range_end   = max(get_end(args),c.size() - 1); 
    if((range_start < 0) || (range_start > range_end)) {
      print("range error!");
      return -1;
    }
    int result = sum_range(c,range_start,range_end); // no more compiler error
    print(result);   
    return 0;
  }

---

StaticAssert and GateKeeper

It is worth noting that StaticAssert only affects a whole component or module at a time - that is, it can't help you with the pieces the compiler can't touch at CompileTime, such as different modules or communications. You'd need true DependentTyping to manifestly state at module interfaces that which one might StaticAssert within the procedural code. With communications (I/O), you're stuck with whatever support the language offers for TypeSafe deserialization (or you need to do-it-yourself).

As such, StaticAssert does not miraculously save you from needing to perform runtime checks. What it DOES do is make it very easy to figure out all the duties of a GateKeeper, since the compiler will keep complaining until the GateKeeper checks all the right things. This allows you to push discovery of input errors very close to the input source and thus minimize the amount of work performed in a failing state. This also helps with optimization, since many of these checks can ultimately be pulled outside of the tight loops that might be found deeper within the module or library.

In a sense, StaticAssert is a form of explicit language support for the GateKeeper pattern. I expect that is how you'd end up using it 90% of the time. However, it also serves a role in code proofs and just ensuring the code to be correct.

---

See KeyLanguageFeature, PartialEvaluation, ProofOptimizer, VerifiedDesignByContract

CategoryFormalMethods