-
Notifications
You must be signed in to change notification settings - Fork 26
Nodes
Pieter edited this page Oct 5, 2022
·
6 revisions
This page describes the structure of the AST ("abstract syntax tree") of COL ("common object language").
Let's start by looking at the anatomy of a node:
-
final
: It's not encouraged to further specialize the behaviour of a node, so we mark concrete nodes final. -
case class
: We maintain the invariant that equal nodes are semantically equivalent. For most nodes, this means that they should define equality structurally, which is implicit for case classes. -
FloorDiv
: Node names should be short but descriptive. Too long:FlooringDivision
, too short:FDiv
, okay:FlooringDiv
. -
[G]
: A type parameter without concrete meaning: it should be propagated into all subnodes. -
(left: Expr[G], right: Expr[G])
: the properties and subnodes of the node. For case classes it is not necessary to specifyval
in the first parameter list. -
(val blame: Blame[DivByZero])
: nodes that are responsible for an error can optionally have an extra parameter list with oneblame
parameter. -
(implicit val o: Origin)
: origins loosely describe the reason a node is in the tree. One simple reason is that it existed in the supplied files. -
extends Expr[G]
: denotes the node family the node belongs to, in this case the expressions. -
with FloorDivImpl[G]
: to keep the file shorter, the implementation of nodes is moved into a trait in a different file.
Tutorial
- Introduction
- Installing and Running VerCors
- Prototypical Verification Language
- Specification Syntax
- Permissions
- GPGPU Verification
- Axiomatic Data Types
- Arrays and Pointers
- Parallel Blocks
- Atomics and Locks
- Process Algebra Models
- Predicates
- Inheritance
- Exceptions & Goto
- VerCors by Error
- VeyMont
- Advanced Concepts
- Annex
- Case Studies
Developing for VerCors