Section Topics




Booleans

Return to Topics

Slang B Type

Slang does not use the Scala Boolean type, but instead provides its own boolean type B and literals T for true and F for false values. Literals true and false are available as well. The primary motivation for this easier reading and writing of truth tables in the truth table sub-language part of Slang that are used in teaching Logical Foundations of Programming.

Slang operators on boolean values are given in the table below (highest precedence first).

B Operators and Precedence

Symbol Operation
!, ~ negation/complement [unary]
== equality
!= inequality
& conjunction (logical and)
&& conditional and (short circuit)
| disjunction (logical or)
|^ logical xor
|| conditional or (short circuit)
imp_:, ->: logical implication [right associative]
simp_:, -->: conditional implication (short circuit), [right associative]

Note

ShortCode: In general, Slang operator precedence follows Scala’s.

Logical vs. Short-Circuit Operators

Conjunction, disjunction, and implication operations characterized as “logical” evaluate both operands, whereas “short circuit” operations evaluate the left operand and evaluate the right operand only when necessary to determine the value of the operation.

Here are some examples:


  println(~F | F)

  // println("F & ((1/0) == 1) :", F & ((1/0) == 1)) // yields run-time exception
  println("F && ((1/0) == 1) :", F && ((1/0) == 1))  // short-circuit avoids exception

  println("T | T :", T | T)     // or
  println("T |^ T :", T |^ T)   // exclusive-or

  println("F |^ T & (!F || ~T) :", F |^ T & (!F || ~T))

  println("Random bool: ", B.random)

produces the following output::

  true
  F && ((1/0) == 1) :false
  T | T :true
  T |^ T :false
  F |^ T & (!F || ~T) :true
  Random bool: false

Random B Values

Each basic type in Slang has a random method associated with it, as illustrated by the B.random operation above. These random methods have an execution semantics, but they play a more important role in specification and verification. During execution, the methods generate a random Slang value of the appropriate type. In Logika verification, declaring a variable with an initial value given by random has the intuition of “introducing a variable whose value you know nothing about”. Similarly, assigning a random value to an existing variable has the effect of removing all constraints from the variable that are being tracked by the underlying deduction engine. Thus, it can be understood as “forgetting/dropping all knowledge about the variable”.


Unbounded Integers

Return to Topics

Slang Z Type

Similar to its dedicated boolean type, Slang introduces its own integer type Z instead of using Scala Int. Z integers are unbounded, unlike the bounded 32-bit Scala Int. The primary motivation for using it is to simplify reasoning about Slang code correctness, in which one does not have worry about overflow and underflow cases in the proof.

Slang does provide a sophisticated collection of bounded numeric types to address its goals of effective compilation to embedded systems (those are addressed later [PENDING: give reference]).

Z Literals

There are several different notations for integer literals, including several that are useful for very large integers. “Conventional” integer literals can be used to state numbers in the interval [-2,147,483,648, 2,147,483,647]. The suffix l or L (e.g., 53,657L) is used to state literals in the range [-9,223,372,036,854,775,808, 9,223,372,036,854,775,807]. 0x can be used to prefix hexadecimal literals. Finally, the format z"<digit string with separators>" is useful for stating very large integers, as illustrated in the examples below:


  println(1) // can express numbers in [-2147483648, 2147483647]
  println(0xFF) // hexadecimal
  println(2L) // use l or L suffix for numbers smaller/larger numbers in [-9223372036854775808,  9223372036854775807]
  println(0xFFl)
  println(z"1000000000000000000000000000000000000000000000") // for any Z number
  println(z"2,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000") // can be separated by comma, underscore, or space (or mixed)
  println(z"3_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000")
  println(z"4 000 000 000 000 000 000 000 000 000 000 000 000 000 000 000")

  println("A random Z: ", Z.random)

  println(1 * 20L + 3 - z"10" / 2l % 10) // arithmetic operators

which produces the following output:


   1
   255
   2
   255
   1000000000000000000000000000000000000000000000
   2000000000000000000000000000000000000000000000
   3000000000000000000000000000000000000000000000
   4000000000000000000000000000000000000000000000
   A random Z: 373512564607001550087401314968846454
   18

Z Operators and Precedence

Slang operators on integer values are given in the table below.

Symbol Operation
- unary negation
*, /, % multiplication, division, modulo
+, - addition, subtraction
==, != equality, inequality
<, <=, >=, > comparison operators

To Do

ShortCode: To Gage: insert some technical remarks about the relationship between Scala integer literals 1 and the fact that the Slang front-end implicitly coerces these to Slang Z types, but sometimes the IVE can get confused and add error markers (even though the code is correct Slang. Note the need to use z"1", etc. in such cases.

The Z Data Type’s Relationship to Scala’s Integer

Since Slang will implicitly understand literal integers e.i. 1 to be of the Z data type, there are times where the front end of the slang or the IVE will confuse the typed literal. In this case, it will produce an error even though the program will still run correctly. However, this confusion can be easily corrected by adapting the literal 1 integer to z"1" an explicit definition of the literal.


Characters

Return to Topics

Slang C Type

Slang introduces its own character type C (32-bit code point) instead of using Scala Char. Character literals are written using single quotes (e.g., 'A', 'q') as opposed to the double quotes used for strings (e.g., "hello", "A" where the last value is a “string A” instead of a “char A”). Unicode literals are using the prefix \u with a four-digit hex value (e.g., \u003F corresponds to '?', \u03A9 corresponds to the Greek letter Omega).

C Operators and Precedence

Symbol Operation
+, - addition, subtraction based on unicode values
==, != equality, inequality
<, <=, >=, > comparison operators
<<, >>>, >> bit shifting operators
&, |, |^ bit and, or, xor operators

Strings

Return to Topics

To Do

ShortCode: To Gage: Try to draft this section. First state the relationship between Strings in Scala and strings in Slang. Then introduce examples of string literals and operators following the style above (look in Robby’s examples for guidance). For any new example snippets you make, add them to the example script files.

Basic String Usage

Printing

In general, a string is just a list of characters. The following are common ways to interact with strings for output.

String Literal:

A literal string can be constructed by surrounding characters in quotation marks.

// # Sireum
import org.sireum._

println("Hello World!") // Prints string starting a new line once finished. Equal to "Hello World!\n" 

Output:

Hello World!
String Variable:

Strings can also be stored in and referred to as variables or values. Variables (var) can be changed after initialization while values (val) can not.

// # Sireum
import org.sireum._

val strVal: String = "Hello"
var strVar: String = "World"

println(strVal)
println(strVar)
print(strVal)
println(strVar)
print(s"${strVal} ${strVar}!")
println()

strVar = "Everyone"
// strVal can not be reassigned.

println(s"${strVal} ${strVar}!")

Output:

Hello
World
HelloWorld
Hello World!
Hello Everyone!
Most Common Print Streams

The two most commonly used print streams are the standard out (stdout) and the standard error (stderr). When using println(), you are using stdout. When you use eprintln(), you are using stderr.

println("Hello, I'm stdout")
println("Hello, I'm stderr")

Output:

Hello, I'm stdout
Hello, I'm stderr **This line will be in RED if it is within the IVE as it is error text.**

Another print option is the method, cprint / cprintln which are conditional print statements. The first argument is a boolean that if true, denotes that the print should be to stderr. If the boolean is false, it will instead print to stdout.

cprintln(false, "I'm false, so I am being printed by stdout!")
cprintln(true, "I'm true, so I am being printed by stderr!")

Output:

I'm false, so I am being printed by stdout!
I'm true, so I am being printed by stderr! **This line will be in RED if it is within the IVE as it is error text.**

All print methods are able to take any number of arguments:

println("Hello")
println("Hello. Is this true? :: ",T==T)
println("Give me a number. ",54," Is that a number? ",T)

Output:

Hello
Hello. Is this true? :: true
Give me a number. 54 Is that a number? true
String Interpolation

String interpolation is the process of where a string is specifically parsed for containing internal values that need to be addressed. For example:

val name: String = "Bob"
println(s"Hello, ${name}!")

val age: Z = 42
println(s"${name} is ${age} years old!")

Output:

Hello, Bob!
Bob is 42 years old!

String interpolation can also be done in multi-line printing

Multi-line Printing

Two ways that multi-line printing can be accomplished is through single-line with escape characters and through multi-line blocks.

Single-Line With Escape Characters

println("Hello!\nNow I'm on a new line.\nWow, a third one...")

Output:

Hello!
Now I'm on a new line.
Wow, a third one...

Multi-Line Blocks

println("""Hello!
Now I'm on a new line.
Wow, a third one...""")

Output:

Hello!
Now I'm on a new line.
Wow, a third one...

Multi-Line Interpolation

For more information on interpolation, see this section

val person: String = "Bob"
val personAge: Z = 46
val isDogOwner: B = true
println(
  s"""Hello, $name!
$name is $personAge years old.
Are they someone who owns a dog? :: $isDogOwner""")

Output:

Hello, Bob!
Bob, is 46 years old.
Are they someone who owns a dog? :: true
Strings / Error Messages in Logical Statements

Both assertions and assumptions can have custom error messages.

//Normal Assert
assert(T)
//With Error Message
assert(T,"error message here")
//

//Normal Assume
assume(T | !T)
//With Error Message
assume(T | !T,"error message here")

Substrings and Characters of Strings:

Since Strings are just a list of characters, we can pull substrings out of a String object.

The substring method of Strings are not able to be used in Slang as they are reserved by Scala. In order for Slang to handle the substring proof internally, there is a separate location for the functionality that is within Slang itself.


 var str: String = "foobar"

 // str.substring(0,3)  **Incorrect, Scala's substring implementation is not in Slang**

val firstStr: String = ops.StringOps(str).substring(0,3) // This is the correct syntax to provide a substring.

// str.substring(3) **Incorrect, Scala's substring implementation is not in Slang**

val lastStr: String = ops.StringOps(str).substring(3,str.size) // This is correct. Notice that Slang's implementation of substring does not have a single argument version of substring. If you are wanting to go from an index to the end of the string, you must denote that index whether it be by a literal or value.

println(str)
println(s"${firstStr} and ${lastStr}")

Output:

foobar
foo and bar

Note

ShortCode: For users accustom to languages that implemented a substring method that includes both a single and two agrument definition, Slang does not have a single argument version of substring’s functionality defined. As such, the two agrument definition must be used. The above example demonstrates one way this can be done.

String Operators and Precedence

Symbol Operation
==, === equality
!=, =!= inequality
<, <=, >=, > comparison operators

Note

Slang does not denote a difference between the operators == and ===. For users that are familiar with Scala, they may recall that the === checks not only for structural equality but ensures that the type of the objects match. In slang, both == and === check for structural equality only. Likewise, there is no difference between != and =!= in Slang.

Note

Also, note that Slang’s Strings are not able to be added or subtracted from one another with a + or - operation.


Reals

Return to Topics

To Do

To Gage: Try to draft this section. Note that reals are idealized, unbounded values, and give some intuition about their underlying representation (to be honest, I wouldn’t know what to say here, so may need to look at the Kekinian source code or ask Robby). Then introduce examples of literals and operators following the style above (look in Robby’s examples for guidance). For any new example snippets you make, add them to the example script files.

the Real data type or R represents an arbitrarily precise decimal number. While floating points (both 32 and 64 bit) have a fixed position, R does not.

Initialization:


val example: R = r"5.0"

// Using 5 or 5.0 instead of r"5.0" will not work as they are integer and double values respectively, and they will not be converted implicitly. The type of an R literal must be explicitly stated, even during instantiation. 

Note

When typing R literals, you must use the form r"0.0". The forms 0 or 0.0 are not implicitly converted to an R value.

The following are examples of basic arithmetic utilizing R values.

val rVal1: R = r"1.0"
val rVal2: R = r"2.0"
val rVal5: R = r"5.0"
val rVal7: R = r"7.5"

println(rVal7+rVal2/rVal7+r"0.489091")
println(rVal1-rVal5*(rVal7-rVal1))
println((rVal7/rVal2)*(r"1.2345"))

Output:

8.255757666666666666666666666666667
-31.50
4.629375
Symbol Operation
- unary negation
*, /, % multiplication, division, modulo
+, - addition, subtraction
==, === equality
!=, =!= inequality
<, <=, >=, > comparison operators

Note

Both == and === only check for structural equality while both != and =!= only check for structural inequality. Neither check for referential equality nor do they check for matching data types. This is because slang does not interact with pointer-type structures, and two unlike data types are not able to be directly equated in the first place.


Floats

Return to Topics

To Do

To Gage: Try to draft this section. Describe the difference between floats and reals. Note the impact on specification and verification (to be honest, I would have to think about this myself some and discuss it with Robby. Basically we need to consider underflow/overflow as well as loss of precision issues that do not occure with reals). Then introduce examples of literals and operators following the style above (look in Robby’s examples for guidance). For any new example snippets you make, add them to the example script files.

To Do

Going to begin by producing a baseline, and can introduce the more specific and difficult issues at another date.

While Reals (R) have arbitrary precision, floats do not. Within Slang there are both 32-bit and 64-bit floats, F32 and F64 respectively.

Initialization:


//Option A: Explicitly convert literal to F32 or F64

val fVal32_a: F32 = f32"4.0" //32-Bit explicit to F32 conversion for literal
val fVal64_a: F64 = f64"4.0" //64-Bit explicit to F64 conversion for literal 

//Option B: Explicitly convert literal to float/double which then is implicitly converted

val fVal32_b: F32 = 4.0f //32-Bit explicit to float conversion for literal (Then implicitly converts to F32)
val fVal64_b: F64 = 4.0 //64-Bit from double to implicitly converted F64

println(fVal32_a)
println(fVal64_a)
println(fVal32_b)
println(fVal64_b)

Output:

4.0
4.0
4.0
4.0

Note

Please note that you must be explicit about the values provided to types in Slang. The Option B statements for F32 and F64 only work as shown above. This is because the F32 data type is constructed from a 32-bit float data type (which the literal is). Likewise, F64’s option b works as its constructor looks for a double data type (which the literal is).

Float values that are 32-Bit, and float values that are 64-Bit are not able to be supplied to the other as Slang will not implicitly convert the value. Likewise, neither will accept an integer value (4).

Example of F32 and F64 Arithmetic:

val a1: F32 = 89.342f
val a2: F32 = f32"592021.3462134"
val a3: F32 = f32"931232343.3423123"
val b1: F64 = 15.32312677
val b2: F64 = 909.3523523456
val b3: F64 = 887187.869809
val flRnd32: F32 = F32.random
val flRnd64: F64 = F64.random

println(s"$flRnd32 (Result will vary)")
println(s"$flRnd64 (Result will vary)")

println(a2 - a1)
println((a3 - a2) * a1)
println((a3 / a1) + a1 % a2)
val x: F32 = (a3 / a1) + (a1*40.65f) / a2
println(x)
println(x*a1-((40.65f*a1*a1)/a2))
println(s"x*a1-((40.65f*a1*a1)/a2) == a3? :: ${(x*a1-((40.65f*a1*a1)/a2)) == a3}")

println(b1 - 16.0)
println(b2 / b1 * b3)
println(b2 % b1 + b3 - 0.2285109 * b2)
val y: F64 = (b3 / b1) + (b1 * 40.65) / b2
println(y)
println(y*b1-((40.65*b1*b1)/b2))
println(s"y*b1-((40.65*b1*b1)/b2) == b3 :: ${y*b1-((40.65*b1*b1)/b2) == b3}")

Output:

0.90476924 (Result will vary)
0.8493481968307036 (Result will vary)
591932.06
8.3145269E10
1.042332E7
1.0423231E7
9.3123232E8
x*a1-((40.65f*a1*a1)/a2) == a3? :: true
-0.67687323
5.2650244854908034E7
886985.3607574641
57899.30339345649
887187.869809
y*b1-((40.65*b1*b1)/b2) == b3 :: true

Underflow/Overflow

To Do

Attempted, but need to verify my observations are true

Underflow and overflow in Slang does not result in wrapping around as overflow does commonly with other data types (such as integers in many languages). Instead, the value is considered F32.PInf for overflow and F32.NInf for underflow if it is an F32 data type. F64 has its own equivalent in F64.PInf and F64.NInf. These values print to Infinity and -Infinity respectively.

Operations that involve the addition or subtraction of two infinities that approach opposite directions, result in NaN (F32.NaN and F64.NaN respectively). This is because infinity is not of a definite or inherently matching size in mathmetics, so the operation can not be accurately determined. This is the reason for the value NaN.

Demonstration

var bigFloat: F32 = F32.PInf
println(s"bigFloat : $bigFloat")
println(s"bigFloat Negated : ${-bigFloat}")
println(s"bigFloat - F32.PInf : ${bigFloat-F32.PInf}")
println(s"bigFloat - F32.NInf : ${bigFloat-F32.NInf}")
println(s"bigFloat + F32.NaN : ${bigFloat+F32.NaN}")
println(s"F32.PInf - F32.PInf : ${F32.PInf-F32.PInf}")
println(s"bigFloat - 1.0 : ${bigFloat-1.0f}")
bigFloat = bigFloat + f32"1.0"
println(s"bigFloat + 1.0 : $bigFloat")

Output:

bigFloat : Infinity
bigFloat Negated : -Infinity
bigFloat - F32.PInf : NaN
bigFloat - F32.NInf : Infinity
bigFloat + F32.NaN : NaN
F32.PInf - F32.PInf : NaN
bigFloat - 1.0 : Infinity
bigFloat + 1.0 : Infinity

Loss of Precision

To Do

Attempted, but need to be checked.

The loss of precision of a float value can happen when a value is rounded due to float values having a fixed precision. For example, 32-bit float values (F32) have six significant values. Any digits after the sixth significant digit are not necessarily accurate. While converting in Slang is possible through the methods within the conversions package (sireum.org.conversions), like other aspects of conversion in Slang, it must be explicit. These conversions do not yet have a built in contract, meaning there is nothing that can be ensured by default from their use. In addition, since F32 values take a Scala float value as the parameter for its constructor and F64 values take a Scala double value as the parameter for its constructor, a valid float, and a valid double can be used to initialize or populate the appropriate types. Likewise, there is no restriction on the number of significant figures that are in the value being interpolated, meaning that if our input value is more significant figures than the maximum promised by the data type, there will be a loss of precision compared to the input value.

Demonstration

println("4621346978291f\n")

println(s"4621346978291f is ${4621346978291f}")

val lopfl: F32 = 4621346978291f
println(s"F32 Value from float : $lopfl")

val lopfl2: F32 = f32"4621346978291"
println(s"F32 Value Interpolation : $lopfl2")

val convertF32toR: R = conversions.F32.toR(lopfl2)
println(s"F32 to R : $convertF32toR")

Output:

4621346978291f

4621346978291f is 4.6213471E12
F32 Value from float : 4.6213471E12
F32 Value Interpolation : 4.6213471E12
F32 to R : 4.62134706176E+12

Operations

Both F32 and F64 have the same operations.

Symbol Operation
- unary negation
*, /, % multiplication, division, modulo
+, - addition, subtraction
==, ===, ~~ equality
!=, =!=, !~ inequality
<, <=, >=, > comparison operators

Note

==, ===, and ~~ all test for structural equality only. !=, =!=, and !~ all test for structural equality only.