creusot icon indicating copy to clipboard operation
creusot copied to clipboard

Published 20 hours ago • verified publisher icon creusot-rs

Creusot User's Guide

Open xldenis opened this issue 2 years ago • 0 comments

Creusot is starting to get large, it would be beneficial to have proper documentation of how to use creusot. This should cover a few key aspects

  1. Pearlite: Syntax, Type systeTm and Semantics. Additionally, a user level explanation of the different operators and how to use them is key to actual usage.
  2. Different function kinds: Explain the different kinds of function logic,predicate, pure and program ones. Also explain the translation of each function, at least at a high level.
  3. Flags like unbounded
  4. Examples of proving and specifying programs: Including common problems / the nitty gritty of how to actually do proofs.

xldenis avatar Oct 14 '21 10:10 xldenis