Skip to content

BaseMax/go-spec-check

Repository files navigation

go-spec-check

A Go-based analyzer that reads structured specifications (states, rules, invariants) and detects contradictions, unreachable states, or incomplete definitions. This tool focuses on logic integrity rather than execution.

Features

  • Contradiction Detection: Identifies conflicting rules and invariants

    • Duplicate state names
    • Contradictory invariants (e.g., true and false)
    • Multiple rules with conflicting conditions for the same transition
  • Unreachable State Detection: Finds states that cannot be reached from the initial state

    • Uses reachability analysis to build a state graph
    • Marks states with no incoming transitions as unreachable
  • Incomplete Definition Checking: Validates specification completeness

    • Missing state names
    • Rules without source or target states
    • Invariants without conditions
    • References to non-existent states (dangling references)

Installation

go get github.com/BaseMax/go-spec-check

Or build from source:

git clone https://github.com/BaseMax/go-spec-check.git
cd go-spec-check
go build -o spec-check ./cmd/spec-check

Usage

Command Line Interface

# Check a specification file
./spec-check -file specification.json

# Verbose output with detailed information
./spec-check -file specification.yaml -verbose

# Output results as JSON
./spec-check -file specification.json -json

As a Library

package main

import (
    "fmt"
    checker "github.com/BaseMax/go-spec-check"
)

func main() {
    // Parse a specification file
    parser := checker.NewParser()
    spec, err := parser.ParseFile("specification.json")
    if err != nil {
        panic(err)
    }

    // Analyze the specification
    analyzer := checker.NewAnalyzer(spec)
    result := analyzer.Analyze()

    // Check results
    if result.Valid {
        fmt.Println("Specification is valid!")
    } else {
        fmt.Printf("Found %d issues\n", len(result.Issues))
        for _, issue := range result.Issues {
            fmt.Printf("[%s] %s: %s\n", issue.Severity, issue.Type, issue.Message)
        }
    }
}

Specification Format

Specifications can be written in JSON or YAML format with the following structure:

Important: The first state in the states array is assumed to be the initial state for reachability analysis.

States

Define the possible states in your system:

{
  "states": [
    {
      "name": "Idle",
      "properties": {
        "description": "System is idle"
      }
    }
  ]
}

Rules

Define transition rules between states:

{
  "rules": [
    {
      "name": "StartProcessing",
      "from_states": ["Idle"],
      "to_state": "Processing",
      "conditions": ["request_received"],
      "description": "Start processing when request arrives"
    }
  ]
}

Invariants

Define conditions that must always hold:

{
  "invariants": [
    {
      "name": "SingleActiveState",
      "condition": "only_one_state_active",
      "applies_to": ["Processing"],
      "description": "Only one state can be active at a time"
    }
  ]
}

Examples

See the examples/ directory for sample specifications:

  • valid-workflow.json - A complete, valid workflow specification
  • unreachable-state.yaml - Demonstrates unreachable state detection
  • invalid-spec.json - Shows various types of errors

Valid Specification Example

{
  "states": [
    {"name": "Start"},
    {"name": "Active"},
    {"name": "Complete"}
  ],
  "rules": [
    {
      "name": "Activate",
      "from_states": ["Start"],
      "to_state": "Active"
    },
    {
      "name": "Finish",
      "from_states": ["Active"],
      "to_state": "Complete"
    }
  ],
  "invariants": [
    {
      "name": "ProgressRequired",
      "condition": "must_eventually_complete"
    }
  ]
}

Issue Types

The analyzer detects the following types of issues:

Type Severity Description
contradiction Error/Warning Conflicting rules, duplicate states, or contradictory invariants
unreachable_state Warning States that cannot be reached from the initial state
incomplete_definition Error Missing required fields or empty definitions
dangling_reference Error References to non-existent states

Testing

Run the test suite:

go test -v ./...

Run tests with coverage:

go test -v -cover ./...

License

This project is licensed under the GPL-3.0 License - see the LICENSE file for details.

Contributing

Contributions are welcome! Please feel free to submit a Pull Request.

About

A Go-based analyzer that reads structured specifications (states, rules, invariants) and detects contradictions, unreachable states, or incomplete definitions. This tool focuses on logic integrity rather than execution. Checks internal consistency of formal specifications.

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

 
 
 

Contributors

Languages