Skip to content

Commit

Permalink
feature: add directive syntax for contract clauses (#4)
Browse files Browse the repository at this point in the history 
Co-authored-by: chavacava <salvador.cavadini@gmail.com>
  • Loading branch information
@chavacava
chavacava and chavacava authored Jan 17, 2025
1 parent 5f2fce6 commit d3574b7
Show file tree
Hide file tree
Showing 4 changed files with 61 additions and 133 deletions.
63 changes: 44 additions & 19 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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`

Expand Down Expand Up @@ -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.

<table>
<tr>
<td> doc friendly contract </td> <td> Raw contract </td>
</tr>
<tr>
<td>

```go
// Contract in standard syntax

// NewCar returns a Car struct.
//
// Contract:
Expand All @@ -246,10 +242,10 @@ While the _raw_ syntax is easier/shorter to write, the _standard_ syntax lets `g
// - requires manufacturer != ""
func NewCar(...) {...}
```
</td>
<td>

```go
// Contract in raw syntax

// NewCar returns a Car struct.
//
// @requires wheels > 2
Expand All @@ -258,11 +254,24 @@ func NewCar(...) {...}
// @requires manufacturer != ""
func NewCar(...) {...}
```
</td>
</tr>
</table>
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

Expand All @@ -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_
33 changes: 5 additions & 28 deletions internal/contract/contract_test.go
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
package contract

import (
"go/ast"
"strings"
"testing"

Expand All @@ -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", "")
Expand All @@ -57,7 +42,7 @@ func TestAddRequires(t *testing.T) {
},
}

c := NewFuncContract(&ast.FuncDecl{})
c := NewFuncContract()
require.NotNil(t, c)

for _, tc := range tests {
Expand All @@ -82,7 +67,7 @@ func TestAddImports(t *testing.T) {
},
}

c := NewFuncContract(&ast.FuncDecl{})
c := NewFuncContract()
require.NotNil(t, c)

for i, tc := range tests {
Expand Down Expand Up @@ -121,7 +106,7 @@ func TestAddLets(t *testing.T) {
},
}

c := NewFuncContract(&ast.FuncDecl{})
c := NewFuncContract()
require.NotNil(t, c)

for _, tc := range tests {
Expand All @@ -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", "")
Expand Down Expand Up @@ -196,7 +173,7 @@ func TestAddEnsures(t *testing.T) {
},
}

c := NewFuncContract(&ast.FuncDecl{})
c := NewFuncContract()
require.NotNil(t, c)

for _, tc := range tests {
Expand Down
13 changes: 10 additions & 3 deletions internal/contract/parser/parser.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -130,8 +130,9 @@ func (p *Parser) parseUnmodified(expr string) (r []contract.Ensures) {
}

var reRawFormatContractClause = regexp.MustCompile(`\s*@(?P<kind>[a-z]+)(?:\s+(?P<description>[\w\s\d,]+): )?\s?(?P<expr>[^$]+)`)
var reDirectiveFormatContractClause = regexp.MustCompile(`\s*contract\:(?P<kind>[a-z]+)(?:\s+(?P<description>[\w\s\d,]+): )?\s?(?P<expr>[^$]+)`)
var reStandardFormatContractClause = regexp.MustCompile(`\s*-\s+(?P<kind>[a-z]+)(?:\s+(?P<description>[\w\s\d,]+): )?\s?(?P<expr>[^$]+)`)
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.
Expand All @@ -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 {
Expand All @@ -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
}
Expand All @@ -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] {
Expand All @@ -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
}
Expand Down
85 changes: 2 additions & 83 deletions internal/contract/parser/parser_test.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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)
}
}

Expand Down

0 comments on commit d3574b7

Please sign in to comment.