This chapter provides an overview of Slang’s class and tuple constructs, which are restrictions of Scala classes and tuples. Closely related notions of trait, object, inheritance, and generics are discussed in subsequent chapters.

Classes

Classes in object-oriented languages like Scala are composite data types that include a fixed set of named data elements (fields) and operations on those elements (methods, functions).

Slang provides constrained use of Scala classes to support:

• a notion of data types (immutable structures) similar to that found in functional programming languages like ML
• records (mutable structures) similar to structures in C and records in Ada, Pascal, etc.

Slang class declarations are annotated with @datatype or @record to indicate the intended kind of structure. Pattern matching is supported for data types and records.

Slang data types are very similar to Scala’s case classes. (see Scala doc) in that they are immutable and equality is structural. Case classes (and Slang data types) are often used when programming in a functional style to create composite structures whose elements are accessed via pattern matching.

Some good examples of this approach occur in applications of the Sireum data modeling framework, which is used in many Slang applications and throughout the Sireum and HAMR infrastructure. In the data modeling framework, Slang data types are used to represent structures such as abstract syntax trees, architectural models, and XML data. In essence, data types are used to define data schemas, and Sireum libraries support serializing/deserializing (to Json) data conforming to the schemas. The Sireum data modeling framework also uses traits (See next chapter), and (Chapter XXX) provides an overview of the framework with extended examples.

Tuples

Both data types and records can be viewed as composite data structures with named elements (fields). Slang also provides tuples – composite data structures with ordered, unnamed elements. Tuples are often used to create a “bundle” of values to return from a method, or in other situations where one needs to create a temporary aggregation of data while avoiding the overhead of creating a class with named fields. Elements of tuples are retreived through pattern matching or through projection operations that refer to the position of elements within the tuple.

Tuples can be either immutable or mutable. In contrast to the explicit qualifiers used to explicitly indicate mutability in Slang data types and records, mutability is determined implicitly for Slang tuples based on the mutability of their constituents. This is in keeping with the goal of having tuples being light-weight (low verbosity declaration and use) composite structures.

Copy-on-demand Semantics

As with the set-theoretic structures of the previous chapter, to avoid creation of aliases, Slang adopts an implicit “copy on demand” semantics when assigning records and mutable tuples to variables or fields. Having a language with a cleaner semantics and easier verification is the motivation for this approach. However, it’s very important for developers and verifiers to be aware of this semantics to correctly reason about the efficiency, memory usage, and verification of Slang mutable structures.