Nereus Language Support for VS Code

DOIs: 10.5281/zenodo.21970707 · 10.5281/zenodo.22072336

Full language support for the Nereus formal algebraic specification language.

Nereus is defined in two open-access books (CC BY 4.0) by Favre, L.:

• Formal Metamodeling for Secure Systems, Zenodo (2025), doi:10.5281/zenodo.21970707 — presents the language, its formal framework for metamodeling in MDE, and the transformations between MOF metamodels and formal specifications.
• The Nereus Language: Syntax, Parsing, and Specification Construction Through Examples, Zenodo (2026), doi:10.5281/zenodo.22072336 — covers the syntax and parsing of the language, and builds specifications step by step through worked examples.

Features

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

File types

.nereus and .nrs

Quick start

1. Open a .nereus file
2. Syntax highlighting appears immediately
3. Diagnostics appear in the Problems panel
4. Hover over any class name or operation for documentation
5. Run Nereus: Show Specification Analysis for the full panel
6. Type class + Tab for a complete class template

Example

CLASS Collection [Elem]
IMPORTS Integer
BASIC CONSTRUCTORS create, add
DEFERRED
TYPE Collection
OPERATIONS
  create: -> Collection;
  add: Collection * Elem -> Collection;
  count: Collection * Elem -> Integer;

EFFECTIVE 
OPERATIONS
  isEmpty: Collection -> Boolean;
  size: Collection -> Integer;
  includes: Collection * Elem -> Boolean;
  excludes: Collection * Elem -> Boolean;
  includesAll: Collection * Collection -> Boolean;
  excludesAll: Collection * Collection -> Boolean;
  forAll: Collection * (Elem -> Boolean) -> Boolean;
  exists: Collection * (Elem -> Boolean) -> Boolean;
  select: Collection * (Elem -> Boolean) -> Collection;
  reject: Collection * (Elem -> Boolean) -> Collection;
  iterate: Collection * (Elem * Acc: ANY -> Acc: ANY) * (-> Acc: ANY) -> Acc: ANY;
  collect: Collection * (Elem -> Elem1: ANY) -> Collection;
  closure: Collection * (Elem -> Collection) -> Collection;

AXIOMS
  c, c1: Collection; e, e1: Elem; f: Elem -> Boolean;
  g: Elem * Acc -> Acc; base: -> Acc; h: Elem -> Collection;
  k: Elem -> Elem1: ANY;

  isEmpty(create()) = True;
  isEmpty(add(c, e)) = False;
  iterate(create(), g, base) = base();
  iterate(add(c, e), g, base) = g(e, iterate(c, g, base));

  LET
    OPERATION f1: Elem * Integer -> Integer;
    AXIOMS e1: Elem; i: Integer;
      f1(e1, i) = if (e = e1) then i + 1 else i endif;
      base() = 0;
    IN
      count(c, e) = iterate(c, f1, base)
  END-LET;

  size(create()) = 0;
  size(add(c, e)) = 1 + size(c);
  includes(create(), e) = False;
  includes(add(c, e), e1) = if e = e1 then True else includes(c, e1) endif;
  excludes(create(), e) = True;
  excludes(add(c, e), e1) = if e = e1 then False else excludes(c, e1) endif;
  includesAll(create(), c) = True;
  includesAll(add(c, e), c1) = includesAll(c, c1) and includes(c1, e);
  excludesAll(create(), c) = True;
  excludesAll(add(c, e), c1) = excludesAll(c, c1) and excludes(c1, e);
  forAll(create(), f) = True;
  forAll(add(c, e), f) = f(e) and forAll(c, f);
  exists(create(), f) = False;
  exists(add(c, e), f) = f(e) or exists(c, f);
  select(create(), f) = create();
  select(add(c, e), f) = if f(e) then add(select(c, f), e) else select(c, f) endif;
  reject(create(), f) = create();
  reject(add(c, e), f) = if not f(e) then add(reject(c, f), e) else reject(c, f) endif;
  closure(create(), h) = create();
  closure(add(c, e), h) = 
    if isEmpty(h(e)) then closure(c, h)
    else add(closure(c, h), h(e))
    endif;
  collect(create(), k) = create();
  collect(add(c, e), k) = add(collect(c, k), k(e));

END-CLASS

This is the complete Collection specification, and it exercises most of what the extension understands: a generic type parameter, the DEFERRED / EFFECTIVE split between the operations a subtype must supply and those derived from them, higher-order operations (forAll, select, iterate, collect, closure), a local LET … IN … END-LET definition, and axioms written by cases over the basic constructors.

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