or run

npx @tessl/cli init
Log in

Version

Tile

Overview

Evals

Files

Files

docs

annotations.mdexceptions.mdindex.md

annotations.mddocs/

0

# Contract Annotations

1

2

Contract annotations define design-by-contract specifications using closure expressions. All annotations are in the `groovy.contracts` package and work with AST transformations to inject runtime assertion checks.

3

4

**Important**: All contract annotations (except `@Contracted`) are marked with `@Incubating`, indicating they are subject to breaking changes in future versions until the API is stabilized.

5

6

## Package Enablement

7

8

### @Contracted

9

10

```groovy { .api }

11

@Target([ElementType.PACKAGE, ElementType.TYPE])

12

@Retention(RetentionPolicy.RUNTIME)

13

@interface Contracted

14

```

15

16

Enables contract processing for packages or classes. Must be applied before using other contract annotations.

17

18

**Usage Example:**

19

20

```groovy

21

@Contracted

22

package com.example.contracts

23

24

import groovy.contracts.*

25

```

26

27

## Class Invariants

28

29

### @Invariant

30

31

```groovy { .api }

32

@Target([ElementType.TYPE])

33

@Retention(RetentionPolicy.RUNTIME)

34

@Repeatable(Invariants.class)

35

@Incubating

36

@interface Invariant {

37

Class value()

38

}

39

```

40

41

Defines class invariants that must hold throughout the object's lifetime. Invariants are checked:

42

- After constructor execution

43

- Before method calls

44

- After method calls

45

46

**Parameters:**

47

- `value`: Closure class containing the invariant condition

48

49

**Contract Rules:**

50

- Can only reference class fields

51

- Combined with parent class invariants using logical AND

52

- Must return boolean or truthy value

53

54

**Usage Examples:**

55

56

```groovy

57

@Invariant({ balance >= 0 })

58

class BankAccount {

59

private BigDecimal balance = BigDecimal.ZERO

60

61

void withdraw(BigDecimal amount) {

62

balance -= amount

63

}

64

}

65

```

66

67

**Multiple Invariants:**

68

69

```groovy

70

@Invariant({ elements != null })

71

@Invariant({ elements.size() >= 0 })

72

@Invariant({ capacity > 0 })

73

class Container {

74

private List elements = []

75

private int capacity = 10

76

}

77

```

78

79

**Inheritance Example:**

80

81

```groovy

82

@Invariant({ name != null })

83

class Person {

84

String name

85

}

86

87

@Invariant({ employeeId != null })

88

class Employee extends Person {

89

String employeeId

90

// Combined invariant: name != null && employeeId != null

91

}

92

```

93

94

## Method Preconditions

95

96

### @Requires

97

98

```groovy { .api }

99

@Target([ElementType.CONSTRUCTOR, ElementType.METHOD])

100

@Retention(RetentionPolicy.RUNTIME)

101

@Repeatable(RequiresConditions.class)

102

@Incubating

103

@interface Requires {

104

Class value()

105

}

106

```

107

108

Defines method preconditions that must be satisfied by callers. Executed as the first statement in method calls.

109

110

**Parameters:**

111

- `value`: Closure class containing the precondition

112

113

**Contract Rules:**

114

- Can reference method arguments and class fields

115

- Combined with parent method preconditions using logical OR (weakening)

116

- Must return boolean or truthy value

117

118

**Usage Examples:**

119

120

```groovy

121

@Requires({ amount > 0 })

122

void deposit(BigDecimal amount) {

123

balance += amount

124

}

125

126

@Requires({ divisor != 0 })

127

@Requires({ dividend != null })

128

BigDecimal divide(BigDecimal dividend, BigDecimal divisor) {

129

return dividend.divide(divisor)

130

}

131

```

132

133

**Multiple Arguments:**

134

135

```groovy

136

@Requires({ startIndex >= 0 && endIndex > startIndex && endIndex <= data.size() })

137

List getSubset(int startIndex, int endIndex) {

138

return data[startIndex..<endIndex]

139

}

140

```

141

142

**Inheritance Example:**

143

144

```groovy

145

class Shape {

146

@Requires({ width > 0 })

147

void setWidth(double width) {

148

this.width = width

149

}

150

}

151

152

class Rectangle extends Shape {

153

@Requires({ width <= maxWidth })

154

@Override

155

void setWidth(double width) {

156

super.setWidth(width)

157

}

158

// Combined precondition: width > 0 || width <= maxWidth

159

}

160

```

161

162

## Method Postconditions

163

164

### @Ensures

165

166

```groovy { .api }

167

@Target([ElementType.CONSTRUCTOR, ElementType.METHOD])

168

@Retention(RetentionPolicy.RUNTIME)

169

@Repeatable(EnsuresConditions.class)

170

@Incubating

171

@interface Ensures {

172

Class value()

173

}

174

```

175

176

Defines method postconditions that guarantee behavior after method execution. Executed after method completion.

177

178

**Parameters:**

179

- `value`: Closure class containing the postcondition

180

181

**Contract Rules:**

182

- Can reference method arguments, class fields, `result`, and `old` values

183

- Combined with parent method postconditions using logical AND (strengthening)

184

- Must return boolean or truthy value

185

186

**Special Variables:**

187

- `result`: Available for non-void methods, contains the return value

188

- `old`: Map containing previous values of cloneable fields

189

190

**Usage Examples:**

191

192

**Basic Postcondition:**

193

194

```groovy

195

@Ensures({ result != null })

196

String formatName(String firstName, String lastName) {

197

return "${firstName} ${lastName}".trim()

198

}

199

```

200

201

**Using Result Variable:**

202

203

```groovy

204

@Ensures({ result >= 0 })

205

@Ensures({ result == old.balance + amount })

206

BigDecimal deposit(BigDecimal amount) {

207

balance += amount

208

return balance

209

}

210

```

211

212

**Using Old Values:**

213

214

```groovy

215

@Ensures({ balance == old.balance - amount })

216

@Ensures({ old.balance >= amount })

217

void withdraw(BigDecimal amount) {

218

balance -= amount

219

}

220

```

221

222

**Constructor Postconditions:**

223

224

```groovy

225

@Ensures({ name != null && name.length() > 0 })

226

@Ensures({ age >= 0 })

227

Person(String name, int age) {

228

this.name = name

229

this.age = age

230

}

231

```

232

233

**Multiple Postconditions:**

234

235

```groovy

236

@Ensures({ result != null })

237

@Ensures({ result.size() <= originalList.size() })

238

@Ensures({ result.every { originalList.contains(it) } })

239

List<String> filterActive(List<String> originalList) {

240

return originalList.findAll { isActive(it) }

241

}

242

```

243

244

## Container Annotations

245

246

### @Invariants

247

248

```groovy { .api }

249

@Target([ElementType.TYPE])

250

@Retention(RetentionPolicy.RUNTIME)

251

@Incubating

252

@interface Invariants {

253

Invariant[] value()

254

}

255

```

256

257

Container for multiple `@Invariant` annotations. Automatically used when multiple `@Invariant` annotations are applied.

258

259

### @RequiresConditions

260

261

```groovy { .api }

262

@Target([ElementType.CONSTRUCTOR, ElementType.METHOD])

263

@Retention(RetentionPolicy.RUNTIME)

264

@Incubating

265

@interface RequiresConditions {

266

Requires[] value()

267

}

268

```

269

270

Container for multiple `@Requires` annotations. Automatically used when multiple `@Requires` annotations are applied.

271

272

### @EnsuresConditions

273

274

```groovy { .api }

275

@Target([ElementType.CONSTRUCTOR, ElementType.METHOD])

276

@Retention(RetentionPolicy.RUNTIME)

277

@Incubating

278

@interface EnsuresConditions {

279

Ensures[] value()

280

}

281

```

282

283

Container for multiple `@Ensures` annotations. Automatically used when multiple `@Ensures` annotations are applied.

284

285

## Best Practices

286

287

### Contract Expression Guidelines

288

289

1. **Keep expressions simple**: Complex logic should be in helper methods

290

2. **Avoid side effects**: Contract expressions should not modify state

291

3. **Use meaningful variable names**: Make contracts self-documenting

292

4. **Test contract violations**: Ensure contracts catch intended violations

293

294

### Performance Considerations

295

296

1. **Use JVM assertion flags**: Control contract checking in production

297

2. **Avoid expensive operations**: Keep contract evaluation lightweight

298

3. **Consider field access patterns**: Minimize field copying for `old` values

299

300

### Inheritance Patterns

301

302

1. **Document contract changes**: Clearly specify how child contracts modify parent behavior

303

2. **Understand combination rules**: Know how preconditions weaken and postconditions strengthen

304

3. **Test inheritance hierarchies**: Verify contract behavior across class hierarchies