The Slang extension mechanism allows Slang to call methods written in other languages supported by Sireum including full Scala, Java, and C.

This enables core high-assurance application code to be written in Slang and analyzed/verified via Sireum tools such as Awas and Logika yet still call low-level drivers (e.g., written in C) or libraries written in Java or Scala.

Here are some common use cases:

• The core of a high-assurance embedded system is written in Slang, but defines extensions that link to C code that interact with sensors, actuators, and embedded OS services. The Slang transpiler is used to compile the Slang core system implementation down to C, and the resulting C is combined with the C for the sensors/actuator extensions and compiled to an embedded executable.

• The core of a high-assurance system is written in Slang, but defines extensions that link to Java or Scala code that provides UI capabilities, enterprise libraries for distributed communication, logging, etc.

Slang extensions implemented in Scala, Java, and C use Sireum provided libaries in the respective language to access Slang data passed to the extension and to create Slang-compatible data to be returned to the Slang caller.

This chapter covers the following activities associated with developing Slang extensions:

• defining interfaces for Slang extension methods

• implementing extensions in Scala

• implementing extensions in Java

• implementing extensions in C