Nereus Language Support for VS Code
Full language support for the Nereus formal algebraic specification language
(Favre, L. Formal Metamodeling for Secure Systems, 2025).
Features
| Feature |
Description |
| Syntax highlighting |
Keywords, types, operators, associations <<Name>>, comments |
| Real-time diagnostics |
Parse errors and semantic warnings as you type |
| Hover documentation |
Type signatures and constructor info on hover |
| Auto-completion |
Keywords, declared classes, operations, attributes |
| Document outline |
Classes, associations, operations in the Explorer sidebar |
| Go to definition |
Navigate to class/operation declarations |
| Analysis panel |
Visual summary: axiom coverage, unknown refs, stats |
| Code snippets |
Templates for CLASS, ASSOCIATION, PACKAGE, LET, pre, … |
| Bracket matching |
(), [], <<>>, /* */ |
Semantic analysis
The extension validates:
- Axiom coverage — every
EFFECTIVE operation has an axiom for each BASIC CONSTRUCTOR
- Constructor signatures — every constructor listed in
BASIC CONSTRUCTORS has an OPERATIONS declaration
- Attribute coverage — every
ATTRIBUTE has axioms covering all constructors
- Type references —
IS-SUBTYPE-OF references are declared classes
- Association coverage —
get_role operations cover all constructors
Commands
| Command |
Description |
Nereus: Show Specification Analysis |
Open visual analysis panel |
Nereus: Check Axiom Coverage |
Quick coverage report in notification |
Nereus: Generate Haxe Code |
Generate Haxe from the current spec |
File types
.nereus and .nrs
Quick start
- Open a
.nereus file
- Syntax highlighting appears immediately
- Diagnostics appear in the Problems panel
- Hover over any class name or operation for documentation
- Run Nereus: Show Specification Analysis for the full panel
- Type
class + Tab for a complete class template
Example
CLASS Stack [elem: ANY]
BASIC CONSTRUCTORS Stack_Empty, Stack_Insert
EFFECTIVE
TYPE Stack
OPERATIONS
Stack_Empty: -> Stack;
Stack_Insert: Stack * elem -> Stack;
Stack_IsEmpty: Stack -> Boolean;
Stack_Top: Stack(p) -> elem
pre: not Stack_IsEmpty(p);
AXIOMS p: Stack; e: elem;
Stack_IsEmpty(Stack_Empty()) = True;
Stack_IsEmpty(Stack_Insert(p, e)) = False;
Stack_Top(Stack_Insert(p, e)) = e;
END-CLASS
Installation from source
git clone <repo>
cd nereus-vscode
npm install
cd server && npm install && npx tsc -p tsconfig.json && cd ..
cd client && npm install && npx tsc -p tsconfig.json && cd ..
# Press F5 in VS Code to launch Extension Development Host
Architecture
nereus-vscode/
├── client/src/extension.ts ← VS Code extension client (LSP client)
├── server/src/
│ ├── nereusParser.ts ← Lexer + recursive-descent parser → AST
│ ├── nereusAnalyzer.ts ← Semantic analysis + symbol table
│ └── server.ts ← LSP server (diagnostics, hover, completion)
├── syntaxes/nereus.tmLanguage.json ← TextMate grammar
├── snippets/nereus.json ← Code snippets
└── language-configuration.json ← Brackets, comments, indentation
| |
