From 9d577dc8a70cb6cd709365f90920f05fa69eb2c5 Mon Sep 17 00:00:00 2001 From: Stevan Andjelkovic Date: Tue, 19 Nov 2024 15:17:37 +0100 Subject: [PATCH] docs: rework readme --- .github/CONTRIBUTING.md | 14 ++ README.md | 391 ++++++---------------------------------- TODO.md | 47 ++--- 3 files changed, 90 insertions(+), 362 deletions(-) diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md index e69de29..88074c7 100644 --- a/.github/CONTRIBUTING.md +++ b/.github/CONTRIBUTING.md @@ -0,0 +1,14 @@ +# Contributing + +There are many ways to help out, here are some examples: + +* Help out with issues and PRs; +* Contribute artwork under appropriate licenses (at least CC-BY-SA); +* Discuss and be helpful to others on: + - IRC in the channel [#spex](https://web.libera.chat/#spex) on `irc.libera.chat`; + - [Zulip](https://spex.zulipchat.com/). +* Contributed to releated projects: + - [`spexup`](https://github.com/spex-lang/spexup), the installer for the Spex + language; + - [`spex-lang.github.io`](https://github.com/spex-lang/spex-lang.github.io), + the Spex language website. diff --git a/README.md b/README.md index 513e1d3..12a0b44 100644 --- a/README.md +++ b/README.md @@ -1,371 +1,84 @@ # Spex -[![Zulip](https://img.shields.io/badge/zulip-join_chat-blue.svg)](https://spex.zulipchat.com/) -[![IRC: #spex on libera.chat](https://img.shields.io/badge/IRC-%23spex%20on%20libera.chat-blue.svg)](https://web.libera.chat/#spex) ![Build status](https://github.com/spex-lang/spex/actions/workflows/main.yaml/badge.svg) -Spex is a specification language and verifier that uses fuzzing and generative -testing techniques to check if software is faithful to some specification. - -It's not a programming language in the traditional sense, meaning that the -software it checks needs to first be written in another language. Another way -to think of it, is that `spex` let's you specify *what* the software under test -should to, but not *how* it does it. - -Currently it only supports specifying and testing HTTP API servers, but the -range of software that can be specified and tested will extended in the -future. +*Spex* is a specification language and toolkit for working with HTTP JSON APIs. +For more information see the [website](https://spex-lang.org). > [!CAUTION] -> Spex is pre-alpha and not suitable for general use yet. Please don't share -> just yet, I'll announce it properly soon. - -## Motivation - -Few people write specifications for their software these days. The reason for -this clear: there are few benefits from doing so, especially when taking into -account the risk of the specification and the real system drifting out of sync -(i.e. either the system or the specification is changed, but we forget to -update the other). - -Spex tries to address this shortcoming of specifications by in addition to -being a specification language, it's also a verifier that checks if some system -respects the specification -- thereby always ensuring that the two are in sync. - -In the process of testing the real system against the specification is will -also produce minimal test cases for potential problems it notices along the way: - - - Non-2xx responses; - - JSON response decoding and type issues; - - Non-reachable APIs. - -(We'll look at examples of how exactly this gets reported in the next section on -features.) - -In the future we'd like to derive more useful functionality from -specifications, including: - - - Ability to import and export OpenAPI/Swagger, Protobuf, etc. Think of how - Pandoc can covert between text formats, perhaps we can do the same between - specifications; - - Generate a prototype implementation from a specification, so that you can - demo your idea or hand of a working server HTTP API to the frontend team - before the actual backend is done (without risking that there will be a - mismatch in the end, since the real backend is tested against the same - specification as the prototype is derived from); - - A REPL, which allows you to explore a system using a specification. Tab - completion is provided for the API and random payload data is generated on - the fly; - - A time traveling debugger which enables you to step forwards and backwards - through a sequence of API calls, in order to explore how the system evolves - over time. - - Lua templating (again similar to Pandoc) which enables code generation from - specifications or the minimal test cases that the verifer produces; - - The ability to refine types, e.g. `{ petId : Int | petId > 0 }` and be able - to generate validation logic from these; - - Generate diagrams for a better overview of how components are connected. - -With this future functionality we hope to get to the point where there's a -clear benefit to writing specifications! - -## Features - -Here are the currently supported features. Click on the "▸ Example" buttons for -more details about how to use them. - -- [x] Concise specification language for HTTP API servers -
- - Example - - ``` - $ cat example/petstore-basic.spex - component PetStore where - - addPet : POST /pet Pet - getPet : GET /pet/{petId : Int} -> Pet - - type Pet = - { petId : Int - , petName : String - } - ``` - -
- -- [x] Ability to test specification against a deployment -
- - Example - - ```bash - $ spex-demo-petstore & - $ PID_PETSTORE=$! - $ spex verify example/petstore-basic.spex - - i Verifying the deployment: http://localhost:8080 - against the specification: example/petstore-basic.spex - - i Checking the specification. - - i Waiting for health check to pass... - - ✓ Health check passed! - - i Starting to run tests... - - ✓ Done testing, here are the results: - - Test failure (3 shrinks): - - 1. getPet : GET /pet/-893 -> Pet - ↳ 404 Not Found - ------------------------------------------------------------------------ - - Coverage: - 2xx: - 49% addPet (49) - 404: - 51% getPet (51) - - Total: 100 - - Use --seed 4254641856041340251 to reproduce - $ kill ${PID_PETSTORE} - [1]+ Terminated spex-demo-petstore - ``` - -
- -- [x] Keep track of previously generated values and sometimes try to use them - during generation of new tests. For example, without this ability the - `getPet` requests would all most certainly return 404. - -- [x] Ability to annotate input types with abstract and unique modalities (@ and - !). Where an abstract type isn't generated, i.e. gets reused, and a unique type - is always generated and never reused. Without any annotation a coin is - flipped and the value either gets reused or generated. -
- - Example - - ```diff - $ diff -u example/petstore-basic.spex example/petstore-modal.spex - - addPet : POST /pet Pet - - getPet : GET /pet/{petId : Int} -> Pet - + addPet : POST /pet !Pet - + getPet : GET /pet/{petId : @Int} -> Pet - $ spex verify example/petstore-modal.spex - - i Verifying the deployment: http://localhost:8080 - against the specification: example/petstore-modal.spex - - i Parsing the specification. - - i Waiting for health check to pass. - - i Starting to run tests. - - i All tests passed, here are the results: - - failing tests: [] - client errors: 3 - coverage: fromList [(OpId "addPet",51),(OpId "getPet",49)] - ``` - - Notice how many fewer 404 errors we get for `getPet` now, because of the - abstract (`@`) annotation on `petId`. -
- -- [x] Keep track of previous responses and try to use them during generation - -
- - Example +> *Spex* is alpha and not suitable for general use yet. Please don't share just +> yet, I'll announce it soon. - Imagine we got: - ``` - addPet : POST /pet Pet - getPet : GET /pet/{petId : Int} -> Pet +## Why Spex? - type Pet = - { petId : Int - , petName : String - } - ``` - and `addPet` is implemented such that it throws an error if we try to add the - exact same pet twice. Finding this error without reusing responses during - generation is difficult, because we'd need to randomly generate the same - `petId : Int` and petname : String` twice. +* OpenAPI [specifications](https://www.openapis.org/), the most common way of + specifying HTTP JSON APIs today, are written in JSON or YAML, both verbose and + error-prone. *Spex* aims to provide a concise specification language which is a + pleasure to read and write, as well as nice error messages that make it easy + to fix mistakes; - If we reuse inputs and reponses on the other hand, then it's easy to find it. - Here's one scenario which would find the error: +* The OpenAPI [tooling](https://tools.openapis.org/) is extensive, and + includes: - 1. We generate a random `Pet` for `addPet`; - 2. A `getPet` operation gets generated that reuses the `petId` from step 1; - 3. The response `Pet` from step 2 gets reused in a subsequent `addPet`, - casuing the error. + - Generation of API clients, server stubs and documentation; + - Testing / fuzzing; + - Mocking; + - Linting. -
+ *Spex*, despite still being young, already has support for fuzzing and + mocking, as well as plans to add code generation, linting and some other + tooling that doesn't have OpenAPI analogues: -- [x] Nice command-line interface and errors for humans + - REPL; + - Debugger. -
+ Finally, one will also be able to import and export OpenAPI specifications, + thereby having access to that ecosystem of tools as well. - Example + By coevolving the language and the tooling, we can add features that will be + hard to replicate in OpenAPI, e.g.: - ``` - $ cat example/petstore-bad-scope.spex - component PetStore where + - Refinement types -- validation logic; + - Model definitions -- fakes rather than mocks and better fuzzing. - addPet : POST /pet Pet - getPet : GET /pet/{petId : Int} -> Pet +* Specifications of the HTTP JSON APIs of components in a system captures how + the components may be called, but they don't say how the components are + related to each other. Longer term *Spex* aims to allow for a wider range of + specifications, e.g. async message passing, as well as means to compose them + into bigger system specifications, this opens up for other kinds of tooling: - $ spex verify example/petstore-bad-scope.spex - i Verifying the deployment: http://localhost:8080 - against the specification: example/petstore-bad-scope.spex + - diagrams - i Checking the specification. +For a more elaborate explaination of the motivation behind *Spex*, see the +following [link](https://spex-lang.org/motivation.html). - Error: Scope error, the type Pet isn't defined. - - ┌─ example/petstore-bad-scope.spex:2:19 - │ - 2 │ addPet : POST /pet Pet - │ ^^^ - - Either define the type or mark it as abstract, in case it shouldn't be - generated. - ``` - -
- -- [x] Test case minimisation aka shrinking -
- - - Example - - - ``` - $ spex verify example/petstore-modal.spex --seed -2917004710203612904 - - i Verifying the deployment: http://localhost:8080 - against the specification: example/petstore-modal.spex - - i Checking the specification. - - i Waiting for health check to pass. - - i Starting to run tests. - - Error: Test failure (8 shrinks): - - 1. addPet : POST /pet {petId = 27, petName = qux} - 2. addPet : POST /pet {petId = 27, petName = qux} - ↳ 409 Conflict: Pet already exists - - Use --seed -2917004710203612904 to reproduce - ``` - Try running with `--no-shrinking` flag to see the original test case that - failed. -
- -- [x] Coverage statistics per operation and response -
- - Example - - ``` - Coverage: - 2xx: - 44% addPet (89) - 54% getPet (107) - 404: - 2% getPet (3) - 409: - 0% addPet (1) - - Total: 200 - - Use --seed 2469868563532480199 to reproduce - ``` - -
- -- [x] Don't stop if a potential problem is found, present all findings at the - end of a test run -
- - Example - - ``` - Test failure: - - 1. getPet : GET /pet/923 -> Pet - ↳ 404 Not Found - ------------------------------------------------------------------------ - Test failure (8 shrinks): - - 1. addPet : POST /pet {petId = 842, petName = foo} - 2. addPet : POST /pet {petId = 842, petName = foo} - ↳ 409 Conflict: Pet already exists - - Use --seed 2469868563532480199 to reproduce - ``` - -
- -- [x] Built-in specifications formatter -
- - Example - - ```bash - $ cat example/petstore-bad-formatting.spex - component PetStore - where +## Installation - addPet : POST - /pet Pet +See [`INSTALL.md`](INSTALL.md) for installation instructions. - getPet :GET /pet/{ petId : - Int} -> - Pet - $ spex format example/petstore-bad-formatting.spex - component PetStore where - - addPet : POST /pet Pet - getPet : GET /pet/{petId : Int} -> Pet - ``` +## Usage -
+The easiest way to get started is to follow the +[tutorial](https://spex-lang.org/tutorial.html). -## Installation +## Community -See [`INSTALL.md`](INSTALL.md) for installation instructions. +If you got any questions or what to discuss what else we can do with +specification, come join one of our chats: -## Usage +* [![Zulip](https://img.shields.io/badge/zulip-join_chat-blue.svg)](https://spex.zulipchat.com/) +* [![IRC: #spex on + libera.chat](https://img.shields.io/badge/IRC-%23spex%20on%20libera.chat-blue.svg)](https://web.libera.chat/#spex) -Click the "▸ Example" buttons in the features list to see examples of how to -invoke `spex`. +Please make sure you follow the [code of conduct](.github/CODE_OF_CONDUCT.md) +when interacting with others. ## Contributing -Spex is at an early stage of development and there are many ways to help out, -here are some examples: - -* Help out with issues and PRs; -* Contribute artwork under appropriate licenses (at least CC-BY-SA); -* Discuss and be helpful to others on: - - IRC in the channel [#spex](https://web.libera.chat/#spex) on `irc.libera.chat`; - - [Zulip](https://spex.zulipchat.com/). -* Contributed to releated projects: - - [`spexup`](https://github.com/spex-lang/spexup), the installer for the Spex - language; - - [`spex-lang.github.io`](https://github.com/spex-lang/spex-lang.github.io), - the Spex language website. +*Spex* is at an early stage of development and is open to various forms of +contribution, see the [`CONTRIBUTING.md`](.github/CONTRIBUTING.md) file for +details. ## License -BSD-style (see the file [`LICENSE`](LICENSE)). +BSD-2-Clause (see the file [`LICENSE`](LICENSE)). diff --git a/TODO.md b/TODO.md index a85da4f..62cb145 100644 --- a/TODO.md +++ b/TODO.md @@ -4,18 +4,13 @@ Here's what I'm currently working on: ### First release -- tests for all examples in readme +- use white bg in logo -- reenable ci for mac and win +- move examples from readme into tutorial - contributing.md + https://x.com/mitchellh/status/1852039089547309552 -- release notes - + focus on infra - + bare minimum language and verifier - + one example, for more see readme/website? - - move todo and roadmap to proper tickets - website @@ -24,24 +19,26 @@ Here's what I'm currently working on: #### Website -+ why/motivation/comparison? - * reachability/coverage - * correct json responses - * minimal test cases that give rise to non-2xx responses -+ install -+ tutorial -+ (docs) ++ index ++ docs + - why/motivation/comparison? + * reachability/coverage + * correct json responses + * minimal test cases that give rise to non-2xx responses + - tutorial + - install + - (faq) + * different from prior work + - https://github.com/microsoft/restler-fuzzer + https://www.code-intelligence.com/blog/stateful-rest-api-fuzzing + - https://github.com/Fuzzapi/API-fuzzer + - https://github.com/KissPeter/APIFuzzer + - https://github.com/TNO-S3/WuppieFuzz + - https://endava.github.io/cats/docs/intro + - https://smithy.io + - [Testing RESTful APIs: A Survey](https://dl.acm.org/doi/10.1145/3617175) + community + (news/blog) -+ (faq) - * different from prior work - - https://github.com/microsoft/restler-fuzzer - https://www.code-intelligence.com/blog/stateful-rest-api-fuzzing - - https://github.com/Fuzzapi/API-fuzzer - - https://github.com/KissPeter/APIFuzzer - - https://github.com/TNO-S3/WuppieFuzz - - https://endava.github.io/cats/docs/intro - - https://smithy.io #### Other @@ -66,6 +63,10 @@ Here's what I'm currently working on: - ensure shrinking shrinks to the same status code, i.e. doesn't uncover another error? +- check for and forbid overlapping ops (same method and path) + +- diff two specs + #### Spexup - cache releases.json?