-
Notifications
You must be signed in to change notification settings - Fork 3
Home
Welcome to the Formula wiki!
FORMULA 2.0 is a novel formal specification language based on open-world logic programs and behavioral types. Its goals are:
(1) succinct specifications of domain-specific abstractions and compilers, (2) efficient reasoning and compilation of input programs, (3) diverse synthesis and fast verification.
We take a unique approach towards achieving these goals: Specifications are written as strongly-typed open-world logic programs. They are highly declarative and easily express rich synthesis verification problems. Automated reasoning is enabled by efficient symbolic execution of logic programs into constraints. We will give a gentle introduction about FORMULA 2.0 language and concepts through four examples. The first two examples of increasing complexity provide demonstrations of basic elements in domains and models, and the command of querying models. The other two examples focus on the transform operation of models. For more detailed syntax and semantics, please refer to the manual.