Specifications

Noir FV programs contain specifications (in the form of annotations) above all functions to define the intended behavior of the code. These specifications include preconditions, postconditions and assertions. Specifications are a form of ghost code — instructions that appear in the Noir program for verification purposes, but are not included in the compiled executable.

This chapter covers the syntax and usage of these specifications through basic examples of preconditions, postconditions, and assertions.