From d3574b72851674764df767a9a4b20dbcfc777b54 Mon Sep 17 00:00:00 2001 From: chavacava Date: Fri, 17 Jan 2025 08:08:43 +0100 Subject: [PATCH] feature: add directive syntax for contract clauses (#4) Co-authored-by: chavacava --- README.md | 63 ++++++++++++------ internal/contract/contract_test.go | 33 ++-------- internal/contract/parser/parser.go | 13 +++- internal/contract/parser/parser_test.go | 85 +------------------------ 4 files changed, 61 insertions(+), 133 deletions(-) diff --git a/README.md b/README.md index 720f8eb..2b79c0a 100644 --- a/README.md +++ b/README.md @@ -32,7 +32,7 @@ Usage of dbc4go: This project is in a pre-ALPHA state. Syntax of contracts might evolve in future versions. -## Available directives to write contracts +## Available contract clauses ### `requires` @@ -222,21 +222,17 @@ func (c *Car) Accelerate(delta int) { ... } ### Contract Syntax -`dbc4go` supports two contract syntaxes: -1. _standard_ syntax, the one introduced in the previous sections, and -2. _raw_ syntax +`dbc4go` supports three contract syntaxes: +1. _standard_ syntax, the one introduced in the previous sections, +2. _raw_ syntax, and +2. _directive_ syntax -Both syntaxes have equivalent expressiveness power. +All three syntaxes have equivalent expressiveness power. While the _raw_ syntax is easier/shorter to write, the _standard_ syntax lets `go` tools to render function and types contracts in a nicer and readable form. - - - - - - - - -
doc friendly contract Raw contract
- ```go +// Contract in standard syntax + // NewCar returns a Car struct. // // Contract: @@ -246,10 +242,10 @@ While the _raw_ syntax is easier/shorter to write, the _standard_ syntax lets `g // - requires manufacturer != "" func NewCar(...) {...} ``` - ```go +// Contract in raw syntax + // NewCar returns a Car struct. // // @requires wheels > 2 @@ -258,11 +254,24 @@ func NewCar(...) {...} // @requires manufacturer != "" func NewCar(...) {...} ``` -
+Raw syntax doesn't require a contract declaration, and contract clauses can be line-interleaved within non-contractual documentation. -Raw syntax does not require a contract declaration, and contract clauses can be interleaved within non-contractual documentation. +Directive syntax is useful in situations where you need to add a contract clause that will not render in the documentation. +For example, if a struct invariant refers to a private field and you don't want to leak the field's name in the documentation you can define the invariant using directive syntax: + +```go +// Contract in directive syntax + +// BankAccount represents a bank account. +// +//contract:invariant !BankAccount.closed ==> BankAccount.balance >= minBalance +//contract:invariant !BankAccount.closed ==> BankAccount.balance <= maxBalance +//contract:invariant BankAccount.closed ==> BankAccount.balance == 0 +type BankAccount struct { + balance int // the balance of the account + closed bool // is the account closed? +} +``` #### Raw syntax summary @@ -272,10 +281,26 @@ Raw syntax does not require a contract declaration, and contract clauses can be `@let` _id_ `:=` _expression_ -`@invariant` _GO Boolean expression_ +`@invariant` [_description_:] _GO Boolean expression_ `@unmodified` _identifiers list_ `@import` _pakage name_ You can **check [these examples](./examples/raw_contracts/)** of code annotated with the raw syntax. + +#### Directive syntax summary + +Contract clauses must respect the directive comment format as defined in the **Syntax** section of [Go Doc Comments](https://tip.golang.org/doc/comment) + +`contract:requires` [_description_:] _GO Boolean expression_ + +`contract:ensures` [_description_:] _GO Boolean expression_ + +`contract:let` _id_ `:=` _expression_ + +`contract:invariant` [_description_:] _GO Boolean expression_ + +`contract:unmodified` _identifiers list_ + +`contract:import` _pakage name_ diff --git a/internal/contract/contract_test.go b/internal/contract/contract_test.go index 6b9ab7f..48a7c65 100644 --- a/internal/contract/contract_test.go +++ b/internal/contract/contract_test.go @@ -1,7 +1,6 @@ package contract import ( - "go/ast" "strings" "testing" @@ -10,32 +9,18 @@ import ( ) func TestConstructor(t *testing.T) { - fd := &ast.FuncDecl{} - - target := fd want := &FuncContract{ requires: []Requires{}, ensures: []Ensures{}, lets: []Let{}, - target: fd, imports: map[string]struct{}{}, } - got := NewFuncContract(target) + got := NewFuncContract() require.NotNil(t, got) assert.Equal(t, got, want) } -func TestTargetGetter(t *testing.T) { - fd := &ast.FuncDecl{} - target := fd - want := target - - got := NewFuncContract(target) - require.NotNil(t, got) - assert.Equal(t, got.Target(), want) -} - func TestAddRequires(t *testing.T) { sampleReq1 := NewRequires("1", "") sampleReq2 := NewRequires("2", "") @@ -57,7 +42,7 @@ func TestAddRequires(t *testing.T) { }, } - c := NewFuncContract(&ast.FuncDecl{}) + c := NewFuncContract() require.NotNil(t, c) for _, tc := range tests { @@ -82,7 +67,7 @@ func TestAddImports(t *testing.T) { }, } - c := NewFuncContract(&ast.FuncDecl{}) + c := NewFuncContract() require.NotNil(t, c) for i, tc := range tests { @@ -121,7 +106,7 @@ func TestAddLets(t *testing.T) { }, } - c := NewFuncContract(&ast.FuncDecl{}) + c := NewFuncContract() require.NotNil(t, c) for _, tc := range tests { @@ -141,14 +126,6 @@ func TestLetGetters(t *testing.T) { assert.Equal(t, descr, let.Description()) } -func TestTarget(t *testing.T) { - fd := &ast.FuncDecl{} - c := FuncContract{target: fd} - - tgt := c.Target() - assert.Equal(t, tgt, fd) -} - func TestRequires(t *testing.T) { sampleReq1 := NewRequires("1", "") sampleReq2 := NewRequires("2", "") @@ -196,7 +173,7 @@ func TestAddEnsures(t *testing.T) { }, } - c := NewFuncContract(&ast.FuncDecl{}) + c := NewFuncContract() require.NotNil(t, c) for _, tc := range tests { diff --git a/internal/contract/parser/parser.go b/internal/contract/parser/parser.go index 93baf7a..314c054 100644 --- a/internal/contract/parser/parser.go +++ b/internal/contract/parser/parser.go @@ -130,8 +130,9 @@ func (p *Parser) parseUnmodified(expr string) (r []contract.Ensures) { } var reRawFormatContractClause = regexp.MustCompile(`\s*@(?P[a-z]+)(?:\s+(?P[\w\s\d,]+): )?\s?(?P[^$]+)`) +var reDirectiveFormatContractClause = regexp.MustCompile(`\s*contract\:(?P[a-z]+)(?:\s+(?P[\w\s\d,]+): )?\s?(?P[^$]+)`) var reStandardFormatContractClause = regexp.MustCompile(`\s*-\s+(?P[a-z]+)(?:\s+(?P[\w\s\d,]+): )?\s?(?P[^$]+)`) -var reStandardFormatContractBlockStarter = regexp.MustCompile(`\s*Contract:\s*$`) +var reStandardFormatContractBlockStarter = regexp.MustCompile(`\s*[Cc]ontract:\s*$`) // parseLine extracts kind, description and expr from a given comment line // If the line is a contract annotation it returns matched true, false otherwise. @@ -140,6 +141,11 @@ var reStandardFormatContractBlockStarter = regexp.MustCompile(`\s*Contract:\s*$` // - ensures matched ==> kind != "" // - ensures matched ==> expr != "" func (p *Parser) parseLine(line string) (kind, description, expr string, matched bool) { + r2 := reDirectiveFormatContractClause.FindAllStringSubmatch(line, -1) + if r2 != nil { + return extractContractPartsFromMatch(r2) + } + if p.currentContractStyle == contractStyleUnknown { r2 := reStandardFormatContractBlockStarter.FindAllStringSubmatch(line, -1) if r2 != nil { @@ -157,7 +163,7 @@ func (p *Parser) parseLine(line string) (kind, description, expr string, matched return extractContractPartsFromMatch(r2) } - r2 := reRawFormatContractClause.FindAllStringSubmatch(line, -1) + r2 = reRawFormatContractClause.FindAllStringSubmatch(line, -1) if r2 == nil { return kind, description, expr, false } @@ -178,7 +184,7 @@ func extractContractPartsFromMatch(match [][]string) (kind, description, expr st description = expr expr = match[0][3] } - return kind, description, expr, true + return kind, description, strings.TrimSpace(expr), true } func (*Parser) canonicalLinesFromComments(comments []*ast.Comment) iter.Seq[string] { @@ -188,6 +194,7 @@ func (*Parser) canonicalLinesFromComments(comments []*ast.Comment) iter.Seq[stri for _, commentLine := range comments { line := strings.TrimLeft(commentLine.Text, "/") line = strings.TrimSpace(line) + if line == "" { continue } diff --git a/internal/contract/parser/parser_test.go b/internal/contract/parser/parser_test.go index be53d21..0dcdd9a 100644 --- a/internal/contract/parser/parser_test.go +++ b/internal/contract/parser/parser_test.go @@ -364,94 +364,13 @@ func TestParseFuncContract(t *testing.T) { "// @unmodified /", "// a", }, - wantContract: contract.NewFuncContract().AddImport(" a"). + wantContract: contract.NewFuncContract().AddImport("a"). AddLet(contract.NewLet("b := true", "")). AddRequires(contract.NewRequires("c != true", "dummy req")). AddEnsures(contract.NewEnsures("@old(d) == d ==> false", "dummy ensures")). AddEnsures(contract.NewEnsures("@old{a} == a", "a unmodified")), wantErr: nil, }, - /* - { - name: "comment with standard invariant", - comments: []string{ - "// TypeFoo is a model for foo", - "// Contract:", - "// - invariant a == a", - }, - wantContract: contract.NewTypeContract(target).AddEnsures( - contract.NewEnsures("a == a", ""), - ).AddRequires( - contract.NewRequires("a == a", ""), - ), - wantErr: nil, - }, - { - name: "comment with @old in standard invariant", - comments: []string{ - "// TypeFoo is a model for foo", - "// Contract:", - `// - invariant a == @old{a}`, - }, - wantContract: contract.NewTypeContract(target), - wantErr: errors.New("@old can not be used in 'invariant' expressions: a == @old{a}"), - }, - { - name: "comment with in standard invariant + import", - comments: []string{ - "// TypeFoo is a model for foo", - "// Contract:", - "// - import math", - "// - import string", - "// - invariant a == a", - }, - wantContract: contract.NewTypeContract(target).AddEnsures( - contract.NewEnsures("a == a", ""), - ).AddRequires( - contract.NewRequires("a == a", ""), - ).AddImport("string").AddImport("math"), - wantErr: nil, - }, - { - name: "comment with invalid @ensure in type contract", - comments: []string{ - "// TypeFoo is a model for foo", - "// Contract:", - "// - ensures a == true", - }, - wantContract: contract.NewTypeContract(target), - wantErr: errors.New("'ensures' can not be used in type contracts: ensures a == true"), - }, - { - name: "comment with invalid @requires in type contract", - comments: []string{ - "// TypeFoo is a model for foo", - "// Contract:", - "// - requires a == true", - }, - wantContract: contract.NewTypeContract(target), - wantErr: errors.New("'requires' can not be used in type contracts: requires a == true"), - }, - { - name: "comment with invalid @unmodified in type contract", - comments: []string{ - "// TypeFoo is a model for foo", - "// Contract:", - "// - unmodified a", - }, - wantContract: contract.NewTypeContract(target), - wantErr: errors.New("'unmodified' can not be used in type contracts: unmodified a"), - }, - { - name: "comment with unknown clause 'unknown' in type contract", - comments: []string{ - "// TypeFoo is a model for foo", - "// Contract:", - "// - unknown a", - }, - wantContract: contract.NewTypeContract(target), - wantErr: errors.New("unknown contract kind unknown"), - },*/ } for _, tc := range tests { @@ -472,7 +391,7 @@ func TestParseFuncContract(t *testing.T) { continue } - assert.Equal(t, tc.wantContract, got, "test %q: contract was not the expexted", tc.name) + assert.Equal(t, tc.wantContract, got, "test %q: contract was not the expected", tc.name) } }