Properties

Properties are CSL functions that describe correctness conditions for CSL code. They serve two purposes:

  1. They help communicate the intended meaning of the code, making it easier to spot mistakes
  2. They can be mechanically checked, helping prevent the introduction of mistakes during development

Often, when writing code, one has a collection of examples in mind. Properties can be used to document these exampels for later use. Properties that represent simple examples are Booleans, with the intention being that they are True when the property holds and False when it does not. In other words, a False property indicates that the code contains a mistake (or that the property itself is incorrect).

val property leapYear2000 = Year::isLeapYear (Year::fromInt 2000)

Properties should be interpreted as statements about the code. In this case, the statement is “the year 2000 is a leap year”.

Properties can also be functions. These properties must return a Boolean value, and their arguments represent “for all” statements. In other words, the property holds if it returns True for all possible argument values.

For example, “converting an Int to a Float and back yields the starting number” can be written as follows:

val property intToFloatToInt = \x -> Float::toInt (Int::toFloat x) = x

Properties may take arbitrary numbers of arguments. For instance, “addition of integers is associative” can be expressed as follows:

val property additionIsAssociative =
    \(x : Int) -> \(y : Int) -> \(z : Int) ->
      x + (y + z) = (x + y) + z
Properties can be used in three ways:
  • Simple Boolean properties are checked to be True.
  • Property functions can be applied to pre-selected lists of arguments.
  • If all arguments are base data types such as Int, or records, unions, or tuples that contain them them, then the CSL tools can randomly generate thousands of test cases, and endure that the property holds for all of them.

Please see the examples repository to see how to do this as part of a standard testing workflow in an application language.