feature: add @UnModified

README.md

@@ -52,21 +52,21 @@ 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 { ... }
 ```
 
 `dbc4go` will generate the following code
 
 ```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 ...

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<kind>[a-z]+)(?:[\t ]+(?P<description>\[[\w\s\d,]+\]))?[\t ]+(?P<expr>[^$]+)`)
 
-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
+}

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")

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
+} 

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
+}