This paper describes the HW-Hume level of the novel Hume language. HW-Hume is the simplest subset of Hume that we have identified. It provides strong formal properties but possesses limited abstraction capabilities. In this paper, we introduce HW-Hume, show some simple example programs, describe an efficient software implementation, and demonstrate how important properties can be exposed as part of an integrated formally-based verification approach.
展开▼
