►The Rosette Guide
▼3 Syntactic Forms
7.7
  top  ← prev  up  next → 

3 Syntactic Forms

The core of the Rosette language (rosette/safe) consists of two kinds of syntax forms: a set of basic forms lifted from Racket, and a set of forms for solver-aided programming. We use the term "lifted" to refer to parts of the Racket language that can be used with symbolic values and other solver-aided constructs.

    3.1 Lifted Racket Forms

    3.2 Solver-Aided Forms

      3.2.1 Symbolic Constants

      3.2.2 Assertions

      3.2.3 Angelic Execution

      3.2.4 Verification

      3.2.5 Synthesis

      3.2.6 Optimization

      3.2.7 Debugging

      3.2.8 Reasoning Precision

  top  ← prev  up  next → 
 
var _hmt = _hmt || []; (function() { var hm = document.createElement("script"); hm.src = "https://hm.baidu.com/hm.js?f1ba5b4a33d29d84db69f029b9ace483"; var s = document.getElementsByTagName("script")[0]; s.parentNode.insertBefore(hm, s); })();