Introduction

This section features some real-world specifications using Gospel and highlights particular features of the language in a concrete setting.

• Fibonacci numbers
  Highlights: Ghost parameters
• Mutable queues
  Highlights: Type models, Exceptional postconditions, requires/checks, consumes
• Union-find.
  Highlights: Ghost declarations