microsoft / microsoft/typespec

Validate/Invariant for models and operations

Open
#2,041 4 comments 1 reaction 1 assignee Claimed by @marron-at-work View on GitHub
Dominant language
Java
Stars
5.9k
Forks
394
Avg merge
1d 23h
Merged PRs (30d)
104

Description

# Problem Overview
Currently TypeSpec provides a standard set of decorators (@minValue, @pattern, etc.) for specifying additional logical properties on data. Developers can also, manually, implement custom decorators for specialized logical concepts. However, there is no simple and expressive way to provide what are traditionally called type/data invariants and operation pre/post conditions.

This issue is intended to be the basis for work on adding functionality to support this scenario via the introduction of explicit keywords for adding invariants to models and pre/post conditions to operations in the form of logical conditions expressed as simple expressions in a programming language. The following sample provides a hypothetical vision of how this might look:

```
model AccountOwner {
name: string;
age: int8;

validate(age > 18, "age is less than 18");
validate(!name::empty(), "empty name is not allowed");
}

model Account {
balance: int32;
kind: "joint" | "single";
owners: AccountOwner[];

validate(kind == "joint" ==> owners::length > 1);
}
```

```
op read(count: int32): string | null
validate(count >= 0, "negative count")
validate(result != null ==> string::length <= count)
;
```
These validate clauses can be processed by emitters to generate executable runtime validation logic as standalone code or part of the parser/validation logic for an application. As they are first class fields in the models/op definitions they can also be annotated with decorators. Two common use cases might be separating validations that are for testing only vs. release mode or identifying validations that are critical to the application correctness vs. that specify some particular implementation behavior that is not semantic version critical:

```
model Account {
accountId: int64;
balance: int32;
kind: "joint" | "single";
owners: AccountOwner[];
transactions: Transaction[];

@release()
validate(kind == "joint" ==> owners::length > 1);

@test()
validate(transactions::allOf((t) => t.sourceAccount == accountId, "Testing -- check all transaction ids match")
}

op read(count: int32): string | null
validate(count >= 0, "negative count")
validate(result != null ==> string::length <= count)

@implementationLimit()
validate(count <= 1024, "Performance is best on small buffers -- please transfer less and 1024 values per request"
;
```
In addition, as outlined below, via a careful construction of the expression language we can ensure that these clauses are in _friendly_ fragments of first-order logic that can be efficiently modeled to discharge checks like -- are the set of validate clauses mutually exclusive, is a change to a clause semver major/minor. We can also build models of values to create inputs that will satisfy them for tasks like fuzzing or automatically generating mocks. Related [issue #961](https://github.com/microsoft/typespec/issues/961).

# Design
The design of this feature involves the addition of 2 keywords (`validate` and `result`), the specification of the expression language syntax, and the semantics/reference implementation of the expression language.

# Tasks
- [x] Add keywords to compiler -- current choice is `validate` and `result` but subject to revision.
- [x] Add support to parse the current Projection expression language as the expression language for the predicates.
- [ ] Add extended operators to support use cases as needed:
- [x] implies ==>
- [ ] Array empty
- [ ] Array someOf/allOf/noneOf
- [x] Array contains
- [ ] Array distinct
- [ ] String empty/startsWith/endsWith/contains

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.