Slang and Logika

This chapter provides an overview of the Slang programming language and its companion Logika contract-based verification tool. This includes high-level discussions of

• the rationale for Slang’s design and its relationship to its “parent” language Scala,
• Slang’s compiler architecture and supported target langugages and platforms,
• Slang’s contract language,
• the Logika verification tool, its architecture, and primary use workflows,
• Slang’s testing infrastructure,
• incorporation of Slang-based development into large-scale development and continuous integration environment, and
• example applications that have been built with Slang and Logika.

These tools are all part of the Kansas State University Computer Science Department SAnToS Laboratory Sireum programming language infrastructure.

While the primary purpose of this material is to give the reader the flavor of the coding, specification, verification, and testing that we cover in these course notes, a secondary purpose is to illustrate that Slang and Logika are powerful tools with wide-ranging capabilities that have been used to build industrial-scale systems.