Packages
Each package is a library written in Cella, published as compiled module packs. A program’s JSON chooses the package:
its lang, and for C++ whether it has a board.
| Package | What it models |
|---|---|
@cella-lang/machine |
The language-neutral execution layer: IEEE 754 binary floating point with correctly rounded operations, fixed-width two’s complement integers, standard streams |
@cella-lang/cfamily |
The core shared by C and C++: the syntax, type checking that reports errors at the node, a small-step semantics over one memory model, the debugger session |
@cella-lang/c |
C11 |
@cella-lang/cpp |
C++17: classes, templates, overloading, references, exceptions, lambdas, and the standard library’s vector and string written in C++ |
@cella-lang/arduino |
Arduino and ESP32/ESP8266 boards on C++: the cores and libraries from their C++ sources, a simulated clock, sensor inputs over time |
@cella-lang/python |
Python: values on a heap, operations and printing that match CPython, exceptions |
@cella-lang/programlogic |
A language-generic program logic: weakest preconditions over a language’s steps and a separation algebra of resources |
How the models are checked
Section titled “How the models are checked”Each model is tested against the real tools: clang with UndefinedBehaviorSanitizer and AddressSanitizer, avr-gcc and the simavr simulator, CPython. For each rule there is a minimal pair of programs, differing in one place, that lands on the two sides of the verdict; removing the rule from the model makes the pair flip.