Name: 'Nereus Formal Specification Language'
Author: 'nereus-ml'

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