diff --git a/README.md b/README.md index f0143e4..373b935 100644 --- a/README.md +++ b/README.md @@ -52,10 +52,10 @@ Example: const maxAuthorizedSpeed = 350 // NewCar returns a Car struct -//@requires wheels > 2 -//@requires wheelsDrive <= wheels && wheelsDrive >= 2 && wheelsDrive%2 == 0 -//@requires maxSpeedKmh > 0 && maxSpeedKmh <= maxAuthorizedSpeed -//@requires manufacturer != "" +// @requires wheels > 2 +// @requires wheelsDrive <= wheels && wheelsDrive >= 2 && wheelsDrive%2 == 0 +// @requires maxSpeedKmh > 0 && maxSpeedKmh <= maxAuthorizedSpeed +// @requires manufacturer != "" func NewCar(wheels int, wheelsDrive int, maxSpeedKmh int, manufacturer string) Car { ... } ``` @@ -63,10 +63,10 @@ func NewCar(wheels int, wheelsDrive int, maxSpeedKmh int, manufacturer string) C ```go // NewCar returns a Car struct -//@requires wheels > 2 -//@requires wheelsDrive <= wheels && wheelsDrive >= 2 && wheelsDrive%2 == 0 -//@requires maxSpeedKmh > 0 && maxSpeedKmh <= maxAuthorizedSpeed -//@requires manufacturer != "" +// @requires wheels > 2 +// @requires wheelsDrive <= wheels && wheelsDrive >= 2 && wheelsDrive%2 == 0 +// @requires maxSpeedKmh > 0 && maxSpeedKmh <= maxAuthorizedSpeed +// @requires manufacturer != "" func NewCar(wheels int, wheelsDrive int, maxSpeedKmh int, manufacturer string) Car { if !(manufacturer != "") { panic("precondition manufacturer != \"\" not satisfied") @@ -101,9 +101,9 @@ Example: ```go // accelerate the car -//@requires delta > 0 -//@requires c.speed + delta <= c.maxSpeedKmh -//@ensures c.speed == @old(c.speed)+delta +// @requires delta > 0 +// @requires c.speed + delta <= c.maxSpeedKmh +// @ensures c.speed == @old(c.speed)+delta func (c *Car) accelerate(delta int) { ... } ``` @@ -114,12 +114,32 @@ The `==>` operator (implication) allows to write more precise and concise contra ```go // accelerate the car -//@requires delta > 0 -//@ensures @old(c.speed) + delta >= c.maxSpeedKmh ==> c.speed == c.maxSpeedKmh -//@ensures @old(c.speed) + delta < c.maxSpeedKmh ==> c.speed == @old(c.speed) + delta +// @requires delta > 0 +// @ensures @old(c.speed) + delta >= c.maxSpeedKmh ==> c.speed == c.maxSpeedKmh +// @ensures @old(c.speed) + delta < c.maxSpeedKmh ==> c.speed == @old(c.speed) + delta func (c *Car) accelerate(delta int) { ... } ``` +### `@unmodified` + +Enforces that the function keeps unmodified the given list of identifiers. + +Syntax: + +`@unmodified` _identifiers list_ + +Example: + +```go +// accelerate the car +// @requires delta > 0 +// @ensures @old(c.speed) + delta >= c.maxSpeedKmh ==> c.speed == c.maxSpeedKmh +// @ensures @old(c.speed) + delta < c.maxSpeedKmh ==> c.speed == @old(c.speed) + delta +// @unmodified c.wheels, c.wheelsDrive, c.maxSpeedKmh, c.manufacturer +func (c *Car) accelerate(delta int) { ... } +``` +`@unmodified` is just syntax sugar for simplify writing `@ensures id == @old(id)` + ### `@import` If in your contracts you need to use a package that is not imported by the original source code, then you can import the package with the `@import` clause. @@ -132,8 +152,8 @@ Example: ```go // Add element e to container -//@import strings -//@requires strings.HasPrefix(e, "my") +// @import strings +// @requires strings.HasPrefix(e, "my") func (c *Container) Add(e string) { ... } ``` @@ -153,8 +173,8 @@ Examples: ```go // Car data-model -//@invariant speed <= maxSpeedKmh type Car struct { + // @invariant speed <= maxSpeedKmh maxSpeedKmh int speed int // other fields ... @@ -163,8 +183,8 @@ type Car struct { ```go // BankAccount data-model -//@invariant balance >= 0 type BankAccount struct { + // @invariant balance >= 0 balance float Owner string // other fields ... diff --git a/internal/contract/parser/parser.go b/internal/contract/parser/parser.go index ed9c9d9..48757a6 100644 --- a/internal/contract/parser/parser.go +++ b/internal/contract/parser/parser.go @@ -6,6 +6,7 @@ package parser import ( "fmt" "regexp" + "strings" "github.com/chavacava/dbc4go/internal/contract" "github.com/pkg/errors" @@ -22,25 +23,6 @@ func NewParser() Parser { var reContracts = regexp.MustCompile(`\s*//\s*@(?P[a-z]+)(?:[\t ]+(?P\[[\w\s\d,]+\]))?[\t ]+(?P[^$]+)`) -func parseLine(line string) (kind, description, expr string, matched bool) { - r2 := reContracts.FindAllStringSubmatch(line, -1) - if r2 == nil { - return kind, description, expr, false - } - - kind = r2[0][1] - expr = r2[0][2] - description = "" - if len(r2[0]) == 4 { - description = expr - expr = r2[0][3] - } - - fmt.Printf(">>>> kind:%q\tdescription:%q\texpr:%q\n", kind, description, expr) - - return kind, description, expr, true -} - // Parse enrich the Contract with the clause if present in the given comment line // @requires contract != nil func (p Parser) Parse(contract *contract.FuncContract, line string) error { @@ -71,6 +53,15 @@ func (p Parser) Parse(contract *contract.FuncContract, line string) error { } contract.AddImport(clause) + case "unmodified": + clauses, err := p.parseUnmodified(expr) + if err != nil { + return errors.Wrap(err, "invalid @import clause") + } + + for _, clause := range clauses { + contract.AddEnsures(clause) + } default: return errors.Errorf("unknown contract kind %s", kind) } @@ -95,3 +86,39 @@ func (Parser) parseRequires(expr, description string) (r contract.Requires, err func (Parser) parseEnsures(expr, description string) (r contract.Ensures, err error) { return contract.NewEnsures(expr, description), nil } + +// @ensures r != nil +// @ensures err == nil +func (p Parser) parseUnmodified(expr string) (r []contract.Ensures, err error) { + result := []contract.Ensures{} + + ids := strings.Split(expr, ",") + for _, id := range ids { + id := strings.TrimSpace(id) + expr := fmt.Sprintf("@old(%s) == %s", id, id) + description := fmt.Sprintf("[%s unmodified]", id) + newEnsure := contract.NewEnsures(expr, description) + result = append(result, newEnsure) + } + + return result, nil +} + +// parseLine extracts kind, description and expr from a given comment line +// If the line is a contract annotation it returns matched true, false otherwise. +func parseLine(line string) (kind, description, expr string, matched bool) { + r2 := reContracts.FindAllStringSubmatch(line, -1) + if r2 == nil { + return kind, description, expr, false + } + + kind = r2[0][1] + expr = r2[0][2] + description = "" + if len(r2[0]) == 4 { + description = expr + expr = r2[0][3] + } + + return kind, description, expr, true +} diff --git a/test/dbc4go_test.go b/test/dbc4go_test.go index 467aed3..39806b4 100644 --- a/test/dbc4go_test.go +++ b/test/dbc4go_test.go @@ -32,6 +32,10 @@ func TestDBC4GO(t *testing.T) { input: "./testdata/4.input", expOutput: "./testdata/4.output", }, + { + input: "./testdata/unmodified.input", + expOutput: "./testdata/unmodified.output", + }, } tmpDir, err := os.MkdirTemp("", "testing-dbc4go") diff --git a/test/testdata/unmodified.input b/test/testdata/unmodified.input new file mode 100644 index 0000000..cb64195 --- /dev/null +++ b/test/testdata/unmodified.input @@ -0,0 +1,12 @@ +package foo + +var a int + +type s struct { + a string +} + +// @unmodified a, s.a +func unmodified(a int, b int) (r int) { + return a +} diff --git a/test/testdata/unmodified.output b/test/testdata/unmodified.output new file mode 100644 index 0000000..7ac745c --- /dev/null +++ b/test/testdata/unmodified.output @@ -0,0 +1,22 @@ +// Code generated by dbc4go, DO NOT EDIT. +package foo + +var a int + +type s struct { + a string +} + +// @unmodified a, s.a +func unmodified(a int, b int) (r int) { + defer func(old_a int, old_b int) { + + if !(old_a == a) { + panic("postcondition @ensures [a unmodified] @old(a) == a not satisfied") + } + if !(old_s.a == s.a) { + panic("postcondition @ensures [s.a unmodified] @old(s.a) == s.a not satisfied") + } + }(a, b) + return a +}