Crate fastbreak 

Fastbreak: A formal methods-inspired specification language

Fastbreak combines ideas from Alloy, TLA+, Cucumber, and Design by Contract to create a specification language that is both formal and readable.

Features

• Type definitions: Define entities and their relationships (Alloy-inspired)
• State machines: Define system states and transitions (TLA+-inspired)
• Scenarios: Given/When/Then executable specifications (Cucumber-inspired)
• Contracts: Preconditions, postconditions, and invariants (DbC-inspired)

Example

module auth

type User {
    id: UserId,
    email: Email,
    status: UserStatus,
}

state AuthSystem {
    users: Set<User>,

    invariant "Users have unique emails" {
        forall u1, u2 in users where u1 != u2 =>
            u1.email != u2.email
    }
}

action register(email: Email) -> Result<User, Error>
    requires { not exists u in users where u.email == email }
    ensures { result is Ok implies result.unwrap() in users' }

Modules

ast

Abstract Syntax Tree for Fastbreak specifications

cli

Command-line interface module

codegen

Code generation module

lexer

Lexical analysis for Fastbreak specifications

model

Compiled specification model

parser

Parser for Fastbreak specifications

project

Project management module

semantic

Semantic analysis for Fastbreak specifications

Structs

SourceLocation

A human-readable source location (1-indexed line and column)

Span

Source location information for error reporting