Introduction

Sparkle is a theorem prover for the functional programming language Clean (version 2.2). It can be used to prove the partial correctness of Clean applications. On a smaller scale, it can also be used to prove useful properties of smaller parts of programs.-

Sparkle has a sophisticated windows-oriented user-interface (meaning that all content is graphically displayed in windows that can be resized, moved and closed at will). The proving process is supported by a hint mechanism, which acts as a proof wizard and suggests proving actions to the user.

Sparkle is written in Clean and is available for download via these webpages.

Features

• Allows reasoning about all programs written in Clean 2.2, except for those that use I/O. Programs are simplified (structure and semantics remain unchanged) before reasoning.
• Properties are expressed in a basic logic, in which the following connectives are available: equality (on expressions), negation, implication, conjunction, disjunction, equivalence (iff), universal quantification and existential quantification. Predicates are not supported (have to be rewritten as decidable predicates that produce booleans).
• 42 different reasoning steps which are mainly inspired by the theorem prover Coq. These tactics are specialized towards functional programming languages. In particular, a reduction mechanism using the functional reduction strategy and an induction mechanism based on algebraic type-definitions are available.
• Three different styles of proving:
  • by typing in a command prompt (powerful, but slow and a lot of knowledge about the reasoning steps available is required),
  • by selecting tactics from a list and producing values for the displayed arguments (powerful, fairly quick, only requires some knowledge about the reasoning steps)
  • by selecting tactics from a suggestion list compiled by Sparkle based on your current goal (not powerful, because only few tactics will be suggested; requires very little expertise, simply trust Sparkle!; many small proofs can be completed using suggestions only!!)
• Proofs are stored as scripts and grouped in sections (a concept similar to modules). Upon restoring sections, the proof scripts will be re-run. Errors will be reported to the user but will only cause the corresponding proof branch to fail.
• An extensive windows-based user interface. All information is displayed in windows that can be closed, moved and resized at will. All opened windows are updated automatically.

Screenshot