HLL

No part of this publication may be reproduced, stored in a retrieval system, or transmitted, in any form or by any means, without the inclusion of the front-page, nor without the inclusion of the present page which includes this legal notice and the history section below.

The authors and the copyright holders of this document make no warranties, neither expressed nor implied, regarding this document or the subject matter described herein, including, but not limited to, warranties of merchantability or fitness for any particular purpose.

While considerable efforts have been made to assure the accuracy of this document and the matter it describes, the authors and the copyright holders will in no event assume responsibility for any direct, indirect, special, incidental or consequential damages resulting from any errors or omissions in the document, including loss of life. The contents of this document may be changed without prior notice.

History

The language HLL was developed by Prover Technology (Prover) from 2008 to 2012 in collaboration with RATP. The language emerged as a successor of the TeclaTool language, which itself was a successor of the Tecla language, both developed by Prover before 2008.

In 2018, HLL 2.7 Logical Foundations Document (LFD) was published on the Internet [1].

Prover renamed and profoundly rewrote the LFD in order to organize it in a more modular way (all aspects of each language construct being grouped together in a single module) with the main purpose of making it easier to ensure the completeness of the language definition. The result was version 3.0 of the document with the new title “HLL Language Definition”.

In 2018 the HLL Forum initiative started as a working group of tool providers and users of HLL. The new features of HLL 3.0 (compared to version 2.7) were developed jointly by the HLL Forum.

Author

Authors of previous versions

Revision History

Version	Date	Reason for change

3.2*	June 16, 2022	This version is identical to 3.2rc1 (which was accepted by technical review 11755) except for the version number and this entry in the revision history.
3.2rc1*	May 13, 2022	Minor change to the lexical structure concerning carriage return and the null character. Clarified that the membership operator is left-associative.
3.1*	March 31, 2022	This version is identical to 3.1rc1 (which was accepted by technical review 11615) except for the version number and this entry in the revision history.
3.1rc1*	March 23, 2022	Addressed issues arising from technical review 11455. Added (CastNamedType) which was missing. Also fixed minor issue 11578 and major issue 11478 concerning the value nil in domains (affecting (DomainAsRange) and (Membership) and leading to the new restriction (QuantDomainNotNil)).
3.0rc11	February 4, 2022	Added a missing reference to the new Appendix C.
3.0rc10	July 5, 2021	Removed (QuantMinMaxDomainNonEmpty) and added nil-behaviour instead for these quantifiers in case the domain is empty. Minor fix regarding the semantics of the domain of SELECT: it is static due to the new restriction (SelectQuantNoItemsDomain). Specified that line-ending comments and pragmas (//, @) are ended by the ’∖n’-character. Added (CollectionStaticFlag) which was missing. Changed the syntax of <quantif_expr> by refactoring out the SELECT case and accordingly removed the restriction (QuantRestrictedDefault) which is no longer needed, and renamed (QuantDefault) as (QuantSelectDefault). Added Appendix C with an overview of restrictions. Plus some other minor fixes and clarifications.
3.0rc9	February 15, 2021	Added authors on page 2. Marked version 3.0rc8 as approved (by the technical reviewers). Added Appendix E with contact details. Changed the document id from T-810712-LFD-HLL to HLL-LDD.
3.0rc8*	January 20, 2021	Forbid the combination of SELECT and $items by introduction of the restriction (SelectQuantNoItemsDomain). Modified (DefDeclaredLhsAssignableRhs) and renamed it (DefRhsTypeAssignableToLhsType). Minor addition to (DefCollectionRhs) regarding the type of collections. Also addressed issues arising from technical review 10609.
3.0rc7	November 18, 2020	Removed the appendix containing the type system. Updated the semantics of branch variables of case expressions (they are now static streams). This fixes issue 10587. Make undeclared and defined variables default to type bool if they are defined using a recursion. Updated the typing of untyped PRE expressions. Simplified the causality restriction for definitions. Updated the type of the SELECT to be the union type of the types of the selected value and the default value (issue 10215). Plus some minor clarifications.
3.0rc6	February 28, 2020	Updated (QuantVarStaticFlag) due to the introduction of $items.
3.0rc5	December 3, 2019	Provided more details for the causality restriction (DefCausality). Clarified the typing of untyped pre expressions. Adding a definition of the many-sorted model. Also added the new features agreed upon by the HLL forum. That is: 1. Unfolding definitions. 2. SELECT operator (as a quantifier expression). 3. A <domain> is allowed to be just "bool" or "int". (The other extensions on this point having already been added in a previous version.) 4. Quantification (including SELECT) over composite streams. 5. Arrays and functions as proof obligations. 6. Extended integer literals (binary and hexadecimal, plus underscores for readability). 7. Always definitions aligned with latch definitions for integer streams (added a check that the value fits in the target type). 8. A new Section 2.2: Logic of Exceptions.
3.0rc4	January 23, 2019	Addressed issues arising from technical review 9089. Redefined $or so that it does not absorb nil.
3.0rc3	September 24, 2018	Addressed issues arising from technical review 8986.
3.0rc2	September 7, 2018	Addressed issues arising from technical review 8868.
3.0rc1	July 17, 2018	Included a type system in appendix.
3.0a	March 8, 2018	Rewritten from scratch with another document structure. Notable changes and additions to HLL include: 1. Added an order on the values of the bool, enum and integer types. 2. Functions over ordered domains are now generalized arrays, and can be used whenever arrays can. 3. Function types are compatible and assignable only if their parameter types are equal (same sets of values). (Issue 1251.) 4. Empty arrays are allowed. 5. Empty integer range types are allowed. 6. Equality and non-equality operators extended to allow any pair of objects with finite number of scalar components. 7. Membership/elementhood extended to allow any scalar type as domain. 8. Added nil as an exceptional value and defined its sources (divisions by zero, array indexing out of bounds, overflows, et.c.) and its propagation (can be absorbed by if-then-else, case, and some Boolean operators and quantifiers). 9. Streams of empty type (including inputs and memories) are now in principle allowed, but such a stream will carry nil in each time step. 10. Removed the “sized” restriction on pre expressions.
2.8	February 21, 2014	issues: 3987. Fix definition of dependency relation for pre. Move misplaced sentence in same subsection. Update the rule references in the text following the enumerated list in the definition of the dependency relation.
2.7*	March 13, 2012	issues: 262. Add missing case for collections in functions defined on types.
2.6	February 24, 2012	issues: 1243, 1244. Modification of the typing rule (case) to forbid multiple occurrence of the same variable in a pattern. Fix rule (c-definition), was two restrictive the assignability condition was missing.
2.5	February 1, 2012	Add a missing check on rules for quantifiers (no simultaneous multi-introduction of an identifier in the scope). Revisit the other rules that already defined this check (lhs-iterators, lhs-parameters, lambda par function and lambda par array). Reorder items in the definition of H in rule system. Add a missing condition on memories and inputs about empty sorts.
2.4	December 19, 2011	New syntax for the with (issue: 1063), Integration of RATP remarks given in FA_12_LFD-HLL_AQL-Prover_03, reorganization of the syntax, introduction of lambda definitions, some precisions about array projection and function application. Issue 1127
2.3	August 23, 2011	Integration of RATP remarks given in FA_Qualif_v04_LFD-HLL_AQL-Prover_01
2.2	May 17, 2011	Issues: 237, 239, 241, 245, 247, 248, 249, 250, 251, 252, 254, 256, 257, 258, 259, 260, 261, 263, 264, 265, 267, 268, 271, 272, 273, 274, 275, 276, 277, 278, 280, 281
2.1	April 28, 2011	Issues: 157, 126, 125, 123, 122, 121, 120, 119, 117, 115, 114, 113, 112, 111, 103, 104, 105, 106, 107, 87, 90, 91, 93
2.0	February 28, 2011	Major extension of the language with: quantifiers, pre, namespaces, functions, sorts and new switch-case.
1.16	November 4, 2010	Improvement of the postfix array type notation specification.
1.15	October 27, 2010	Fix BNF, the terminating ”s” was missing for the keyword ”obligations”.
1.14	September 20, 2010	Change static flag for cast; this operator is not consider as static anymore. Change the semantics of memories constrained by an implementation type, the implicit cast is removed.
1.13	January 18, 2010	Add a comment to the typing rule of definitions, as recommended by RATP in FA-03_LFD-HLL_rqs_RATP.
1.12	December 30, 2009	Integration of RATP remarks in FA-03_LFD-HLL_rqs_RATP. Modification of the syntax to allow uncapitalised section names, as raised by the parser review.
1.11	November 12, 2009	Minor spelling corrections.
1.10	October 5, 2009	Adding missing rules for type int and collections. Fix the constraints in rules (int-signed) and (int-unsigned), were shifted.
1.9	September 14, 2009	Introduction of tags for the requirements. Fixes of issues found by the validation activity. Revisit the typing rule (Case with Default) to make explicit that cases values are pairwise different. Fix (array-declaration) rule, sizes must be constant.
1.8	June 8, 2009	Introduction of tags for the requirements. Fixes of issues found by the validation activity.
1.7	April 17, 2009	Modification of the semantics of integer memories, it depends now on the way it is declared (a range or an implementation type). Improvement of the presentation of integer types. Integration of the feedbacks from the approbation team (iteration 3).
1.6	April 7, 2009	change the associativity of the power operator, now it associates to the right.
1.5	April 7, 2009	Integration of the feedbacks from the approbation team (iteration 2).
1.4	April 4, 2009	Integration of the feedbacks from the approbation team.
1.3	March 30, 2009	Fix typos, revisit the section about other static checks.
1.2	March 27, 2009	Fix a lot of typos found by peer review.
1.1	March 20, 2009	Remove operator ← (left implication) Change the associativity of i →, now it is right associative. Complete the HLL semantics.
1.0	March 19, 2008	Initial Version.

1 Introduction

This document presents the syntactical and semantical aspects of the HLL¹ modelling language.

HLL is a declarative stream-based language with a large panel of types and operators. It is suitable for modelling discrete-time sequential behaviours and expressing temporal properties of these behaviours.

1.1 Purpose

The purpose of the document is to provide a formal definition of all aspects of HLL in order to be used for the implementation of tools considering this language as a source or a target.

1.2 Definitions, Terms and Abbreviations

1.3 Overview

2 Preliminaries

2.1 Streams

HLL is a language based on the notion of Streams. A stream s represents an infinite sequence of values, one for each time step:

s : s₀ s₁ s₂ s₃ … s_n s_n+1 …

Streams are typed, and the type of a stream can be understood as just a set of values. For example the Boolean type (written bool in HLL) is the set of values {false,true}. The values s_i of the stream s are thus members of the type of s. HLL supports a large number of different types, for example Boolean, integer, enum, struct and array.

The combinatorial operators that can be applied to values of a type T can be lifted to streams of type T by point-wise application in each time step. For example, if a and b are integer streams:

a : a₀ a₁ a₂ … a_n …
b : b₀ b₁ b₂ … b_n …

a + b : a₀ + b₀ a₁ + b₁ a₂ + b₂ … a_n + b_n …

a : 2 3 5 7 11 13 …
b : 1 1 2 3 5 8 …

a + b : 3 4 7 10 16 21 …

It is important to note that lifting a combinatorial operator (like the example above) to the stream level does not make it a temporal operator: in each time step the lifted combinatorial operator has only access to the values in the current time step of its stream operands. A temporal operator, on the other hand, is free to access the entire stream of values of its operands. The X operator (read “next operator”) is an example of a temporal operator which is usually thought of as returning the “next value” of its stream operand. To be precise however, the X operator returns a stream which is shifted one step to the left relative to its operand. To continue our example:

X(a + b) : 4 7 10 16 21 …

In Section 10 the semantics of the HLL nonterminal <expr> is defined using streams (an <expr> is a stream). Therefore we will use the term stream both for the concept described above and for any HLL expression <expr>.

In the following sections we will introduce some concepts and aspects of streams, which will be used to define the semantics of HLL. The most central concept is the (typed) stream model M_T which is just a mapping from a pair (stream of type T, time step) to a value of the type T, or nil (which is an exceptional value used to model undefined behaviour such as a division by zero). For example, Mint applied to the stream a of type int above would return the following values:

Mint(a,0) = 2
Mint(a,1) = 3
Mint(a,2) = 5
.
..

2.1.1 Models

2.1.2 Exceptional Value

2.1.3 Propositions

2.1.4 Consequences

(An alternative term for “model” is “scenario” (such as a counterexample), and the formal definition above simply states that all those, and only those, scenarios (or models) which do not falsify any of the propositions in P need to satisfy the proposition q in order for the latter to be a consequence of the former. We can think of the propositions P as the set of constraints in an HLL text H, and the proposition q as a proof obligation. The problem of deciding whether q is a consequence of P is known as “model checking” ², and it amounts to checking the formula (1) above for all models. If there is no counter-model M to (1), we say that H is a model for q (q is true in H). Admittedly, the use of the word “model” for different purposes may be confusing, but it has historical reasons, and for the purposes of this document it is enough to consider a “model” to be synonymous with “scenario”.)

2.1.5 Static Flag

The static flag is used to restrict the set of possible HLL types and stream expressions.

In Section 10.4 we extend the static flag to domains (nonterminal <domain>), which are streams of sets of values, and in Section 12 we extend it to collections of streams (nonterminal <collection>).

2.2 Logic of Exceptions

In HLL, many operations such as division by zero, overflow, array indexing out of bounds et.c., give rise to the exceptional value nil introduced in Section 2.1.2.

This exceptional value, nil, propagates unhindered through most HLL operations, but are absorbed by a few, such as the if-then-else and the Boolean operations with absorbing values (and, or, implication). In order to preserve the commutativity of the Boolean operators, they are defined to be symmetric in the sense that nil can be absorbed on either side of the operator³ . (This means that “true or nil” and “nil or true” both mean “true”.)

We note, however, that any implementation of HLL which lets nil propagate more freely, and for example reduces “nil or true” to nil instead of “true”, is still safe due to the fact that nil is accepted by

_w on the left hand side of the consequence relation defined by formula (1) in Section 2.1.4 above, whereas it is rejected by

_s on the right hand side. This asymmetry in the consequence relation ensures that an implementation which propagates nil more freely will accept more models in the antecedent and less models in the consequent making it strictly harder to satisfy formula (1).

2.3 Namespaces and Scoping

In HLL, names (identifiers) reside in different namespaces depending on which kind of entity they name. (This means that entities of different kind may have the same name within the same scope, as explained below.) The different kinds of entities and their corresponding namespaces are:

For each of the first three kinds of entities in the list above, there is a single namespace, whereas for struct components, there is one namespace per struct type.

A namespace can (at some fixed point in an HLL text) be divided into scopes, which are stacked downwards one upon the other. A namespace, in this document, is thus not a single set of names, but rather a collection of sets of names, one for each scope.

Assume such a scope stack, for example [S₁ S₂ … S_n] where S₁ is the top-level scope and S_n is the bottom-most scope (the “current” scope), and some element S_i with i ∈ [1,n]. We will call a scope S_j with j < i an Ascendant scope of S_i, and we will call a scope S_k with k > i a Descendant scope of S_i. Note that the scopes S₁…S_i−1 constitute all the ascendant scopes of S_i whereas the scopes S_i+1…S_n only constitute a subset of the descendant scopes of S_i since some of these scopes may have other descendant scopes at other points in the HLL text.

The entities that are Visible (i.e. that can be referenced) in a given scope are those that exist in that scope or in one above it (an ascendant scope).

Names must be unique⁴ within a given scope of a namespace, i.e. two different entities existing in the same scope of a namespace cannot have the same name. However, Hiding is allowed (but not encouraged), meaning that an entity E₁ may have the same name as another visible entity E₂ that exists in an ascendant scope (one higher up in the stack). In such a case we say that E₁ Hides E₂ in all scopes in which E₁ is visible.

It is important not to confuse “namespace” with “user namespace”; the former is the abstract concept described above, the latter is a concrete concept of HLL which is defined in Section 5.

Scopes are introduced by language constructs such as user namespaces, lambda expressions (Section 10.2), case expressions (Section 10.7.9) and quantifier expressions (Section 10.7.10). The formal descriptions of those constructs define the start and end points of the scopes they introduce, and the namespaces the scopes operate on.

Scopes introduced by user namespaces differ slightly from the scopes introduced by the other aforementioned language constructs, in that the entities inside the former can be referenced from the outside by using a path identifier (Section 5.1), whereas the entities inside the latter can be referenced only within the same scope or a descendant one. These referencing rules are formally defined in Section 5.1.

The namespaces containing struct components are not subdivided into scopes, since each struct type introduces its own namespace for the components, as formalised in Section 8.2.2.

2.4 Notation

See Appendix D for a comprehensive list of words, terms and abbreviations used within this document.

2.4.1 Syntax-Related Notation

For the terminals that are described with a regular expression, the right-hand side of the rule starts with regexp:.

2.4.2 Semantics-Related Notation

We will use (mostly uppercase) letters in This Font to denote variables representing nonterminals (i.e. syntactic variables). For example, V, T and E are typically used to represent respectively the nonterminals <id> (Section 4), <type> (Section 8) and <expr> (Section 10). However, often we simply use the nonterminal itself for the same purpose.

In a slight abuse of notation (but in an effort to ensure visual coherency), we extend the use of these symbols to also denote semantic entities in general (even if they do not have a concrete HLL syntax), for example the letter T is used throughout the document to denote any type, even one which does not have an explicit HLL syntax (see Section 8.4 for examples).

In order to have a compact definition of HLL, the semantics of the various language constructs is often defined by translation to other, more basic or general, language constructs.

Typically, for a language contruct C₁ and a more basic language contruct C₂, we will use the following two relations to relate C₁ to C₂:

To avoid redundancy, whenever we say that C₁ is equivalent or reducible to C₂ this means that all relevant restrictions that apply to C₂ (directly or indirectly), also apply to C₁, even if this is not explicitly said. Furthermore, if C₁ and C₂ are expressions they will have the same type even if this is not explicitly said.

As an example, the expression E₁ != E₂ is defined as equivalent to ~(E₁ = E₂). This means that the relevant restriction that says that the operands of = be of “compatible types with a finite number of scalar components” also applies to operator !=. By contrast, the restriction that says that the operand of ~ be of type bool is irrelevant, and does not apply to operator !=.

To be more precise about which restrictions are relevant, one should consider a “language construct” as being a function from one or more explicitly grouped HLL strings to a single explicitly grouped HLL string. For example, if we let = denote the function EQ(<expr>,<expr>) ⇒ (<expr> = <expr>), and ~ the function NOT(<expr>) ⇒ ~<expr>, then we can define != as being equivalent to the function composition NOT∘EQ (i.e. first apply EQ then NOT). The restrictions that apply to the domain of definition of != are thus those that apply to the domain of definition of NOT∘EQ (which is the same as the domain of EQ).

If a language construct C₁ has additional restrictions compared to another construct C₂, but they are otherwise equivalent, we will typically say that C₁ is reducible to C₂. As an example, the expression E₁ <-> E₂ is reducible to E₁ = E₂ since the type bool required of the operands of <-> satisfies the restrictions on =, but not the other way around.

Occasionally, we will use the relation “C₁ is equivalent to C₂ except for some property P”. This means, naturally, that the semantics of C₁ and C₂ is identical except with regards to the property P (which is of minor importance). This relation will be used whenever neither of C₁ and C₂ is reducible to the other, but the semantics of the language constructs are still closely related.

2.5 Document Structure

This document has been structured around the syntax of HLL⁶ . The syntax, semantics and restrictions for each set of closely related nonterminals of the language are grouped together whenever possible and the resulting groups are sorted with the goal of minimizing forward references. Each such group is placed in its own section that may contain a short introduction with a few examples followed by a formal definition. Please note that the introduction and examples are only intended as a help to understand the formal definition.

2.5.1 Language Construct Example

Here we may give a short informal introduction with a few examples as a help for the reader. Below, in the blue box, follows the formal definition. The labels (ExampleSyntax), (ExampleSemantics) and (ExampleRestriction) can be used for referencing purposes either within this document or another one. An index of labels can be found in Appendix D.

Syntax

(ExampleSyntax)

  <nonterminal1> ::= <nonterminal2>
                   | <nonterminal3>
  <nonterminal2> ::= "terminal1" <nonterminal4> "terminal2"

Forward References

1.: Here we give references to the definitions of the nonterminals appearing on the right hand side of a nonterminal definition and defined in a subsequent section of the document. Note that nonterminals which are defined in a subsequent subsection of the present section are not listed here.

Semantics

1.: (ExampleSemantics) Here we define the semantics (meaning) of all nonterminals appearing on the left hand side of a nonterminal definition above. In this case it means <nonterminal1> and <nonterminal2>.

Restrictions

1.: (ExampleRestriction) Here we list all the cases of HLL strings which are valid syntactically, but still not part of the language.

Related Notation

1.: Here we will sometimes introduce notation related to the current language construct, that is to be used elsewhere in the document.

3 Lexical Structure

Characters in an HLL text shall be encoded in ASCII, or any 8-bit extension of it. The following characters are not allowed in an HLL text:

The following characters or character sequences may be inserted freely anywhere between terminals in an HLL text:

Comments and pragmas, defined below, may also be inserted freely between terminals.

3.1 Comments

Informal Description

3.2 Pragmas

Informal Description

4 Identifiers

Syntax

(IdSyntax)

<id>      ::= regexp: [a-zA-Z_][a-zA-Z0-9_]*
            | regexp: ’[^\n’]+’
            | regexp: "[^\n"]+"

Semantics

1.: (Id) An identifier (<id>) identifies a named entity of an HLL text by its name, where an entity is either either a type, a stream, a struct component or a user namespace. An identifier may be used either to give an entity its name (by a declaration or definition), or to refer to an existing named entity. In a few cases a reference to a nonexisting entity may cause the entity to exist. This is called implicit declaration by reference.
2.: (IdSignificantChars) Identifiers are case sensitive and all characters (including quotes) of an identifier are significant.

Restrictions

1.: (ReservedWords) An <id> may not be a reserved word. The reserved words are listed in Appendix B.

5 User Namespaces

Syntax

(NamespaceSyntax)

<namespace> ::= <id> "{" <HLL> "}"

Forward References

1.: <HLL> is defined in Section 16.

Semantics

1.: (UserNamespace) A User namespace (<namespace>) is a named container for names of an <HLL> text, meaning that names contained in different user namespaces will not clash. More precisely, a user namespace N { HLL } introduces local scopes in the namespaces of streams, types and user namespaces that start at the { and ends at the }. These local scopes are called the top-level scopes of the user namespace, and are not to be confused with the global top-level scopes.
2.: (UserNamespaceName) The <id> defines the name of the namespace and it resides in the namespace of user namespaces.
3.: (UserNamespaceScattering) Two <namespace> in the same scope and with the same <id> refers to the same user namespace. This means that N { HLL₁ } … N { HLL₂ } (where … represents anything in the text that may come in between of the two <namespace>) is equivalent to N { HLL₁ HLL₂ }.

Restrictions

5.1 Path Identifiers

Path identifiers allow referencing named types or streams in any user namespace (all top-level members of a user namespace are public and can be referenced from the outside). An example:

⁷In this case, if there is no NS₁ on the global top-level then the corresponding <path_id> is invalid.

Syntax

(PathIdSyntax)

<path_id>       ::= <relative_path> <id>
                  | <absolute_path> <id>
<relative_path> ::= { <id> "::" }
<absolute_path> ::= "::" { <id> "::" }

Semantics

1.

(PathId) A <path_id> refers to an entity with name <id> in some user namespace (or on global top-level) designated by an optional prefix which is either a Relative path (<relative_path>) or an Absolute path (<absolute_path>). An empty prefix designates either the user namespace in which the <path_id> occurs or else the global top-level (if the <path_id> occurs there).

2.

(PathRelative) A <relative_path> NS₁ :: NS₂ :: … :: NS_n :: designates a user namespace NS_n that is nested inside user namespaces NS₁…NS_n−1 where NS₁ is selected by applying the following rules in order:

(a): If the <relative_path> occurs in a user namespace N and N has a directly nested user namespace NS₁, then this NS₁ is selected.
(b): Otherwise, the user namespace NS₁ defined on the global top-level is selected⁷.

3.

(PathAbsolute) An <absolute_path> :: NS₁ :: NS₂ :: … :: NS_n :: designates a user namespace NS_n that is nested inside user namespaces NS₁…NS_n−1 where NS₁ is defined on the global top-level.

4.

(PathIdLookup) Given a <path_id> [PATH::]ID, the following rules are applied to lookup the entity E with the name ID:

(a): If no PATH is given, then the scope stack to consider for the search is the maximal one ending where the <path_id> occurs, i.e. [S₁ S₂ … S_n], where S₁ corresponds to the global top-level and S_n corresponds to the current (bottom- or inner-most) scope.
(b): If a PATH is given, then the search for ID is made only at the top-level⁸ scope S_PATH of the user namespace designated by PATH. The scope stack to consider for the search is thus [S_PATH].
(c): Given a scope stack [S₁ S₂ … S_k] as determined from cases 4a and 4b, the search for ID starts in S_k and then proceeds in the order S_k−1,S_k−2,…S₂,S₁. The search stops as soon as an entity E with the name ID is encountered in one of the S_i, and it is this entity E which the <path_id> refers to. The semantics or correctness of a <path_id> that does not refer to any existing entity E depends on the context in which the <path_id> is used. The general rule is that such a <path_id> is incorrect, and the only exception to this rule are unqualified named expressions, which implicitly declare the nonexisting stream variables they refer to, causing them to exist (see (NamedExprImplicitDecl) of Section 10.7.3).

Restrictions

1.: (PathIdNoImplicitDecl) A qualified <path_id> (i.e. a <path_id> with at least one occurrence of ::) shall refer to an existing entity (no implicit declaration by reference).

⁸This means that the path identifiers i and N :: i in the lambda expression below do not refer to the same entity named i, since the first one refers to the lambda parameter and the second one to the input variable.

6 Lists

Syntax

<id_list>   ::= <id> {"," <id>}

<type_list> ::= <type> {"," <type>}

<expr_list> ::= <expr> {"," <expr>}

Forward References

1.: <type> is defined in Section 8.
2.: <expr> is defined in Section 10.

Semantics

Restrictions

7 Declarators

Declarators in HLL provide a way to declare objects of array and function type that reflects the use of the objects. For example:

An equivalent notation, shown below, is the array-type notation introduced in Section 8.2.4, and it is this rewriting from declarators to proper type notation that is performed by the function calc_type on the next page.

An analogue example can be made using function declarators and function-type notation, for example the declaration bool f(int) corresponds to the declaration (int -> bool) f using the function-type notation introduced in Section 8.2.3.

Note that for multidimensional arrays the syntax bool A[4, 3] can be used instead of bool A[4][3] above (the corresponding array-type notation is then bool^(4, 3)). The two ways to express multidimensionality are similar but not equivalent. The same is true of functions: in HLL we can both have a function taking several parameters (called a multivariate function) or a function returning another function.

Declarators can be used also in type definitions, as shown in the example below, which is an equivalent formulation of our example above:

Syntax

(DeclaratorSyntax)

<declarator>        ::= <id> {<declarator_suffix>}
<declarator_suffix> ::= "[" <expr_list> "]"
                      | "(" <type_list> ")"

Semantics

1.

(Declarator) A Declarator (<declarator>) consists of an identifier <id> and an optional declarator suffix (<declarator_suffix>).

2.

(DeclaratorTypeCalc) The recursive function calc_type defined below takes as input a base type T (a <type>) and a list of <declarator_suffix> D and returns an augmented type (which is typically associated with the identifier <id> of the corresponding <declarator>, if any). Note that the base type T is not provided from a <declarator>. Instead it typically comes from an enclosing syntactic rule. See for example <type_def> in Section 8.

calc_type(<type> T, {<declarator_suffix>} D) { let L be the last <declarator_suffix> of D and let D∖L denote D without L in : if L is [E₁, E₂,…E_n] : return calc_type(T (E₁, E₂,…E_n), D∖L). else if L is (T₁, T₂,…T_n) : return calc_type((T₁ ∗T₂ ∗…∗T_n -> T), D∖L). else (D is empty) : return T. }

Please note that the array type notation T (E₁, E₂,…E_n) is defined in Section 8.2.4 and the function type notation (T₁ ∗T₂ ∗…∗T_n -> T) in Section 8.2.3.

Restrictions

1.: (DeclArrayDimInteger) Each E_i of a declarator suffix [E₁, E₂,…E_n] shall be of integer type (see Section 8.1.2).
2.: (DeclArrayDimConstant) 𝒮ℱ(E_i) = 2 for a declarator suffix [E₁, E₂,…E_n].
3.: (DeclFunctionParamScalar) Each T_i of a declarator suffix (T₁, T₂,…T_n) shall be scalar (see Section 8.1).

8 Types

Types in HLL should be understood as sets of values. As an example the Boolean type (written bool) is the set {false,true}. Types are assigned to stream variables (named streams) either by explicit declaration (see Section 11), by inference (see (DefUndeclaredType) of Section 12), or in rare cases by reference (see (NamedExprImplicitDecl) of Section 10.7.3). Types are assigned to stream expressions (unnamed streams) by type inference based on the operator and the types of operands (if the operator is overloaded to handle more than one type of operands). The precise typing rules are given in connection with the definition of the expressions’ semantics (i.e. throughout Section 10).

A stream can only take values of its assigned type (regardless of how the stream was assigned the type), or the exceptional value nil in response to an exceptional event such as a division by zero or an overflow.

⁹We will treat nil as a truly exceptional value that does not belong to the types propers.

Syntax

(TypeSyntax)

<type>      ::= <bool>
              | <integer>
              | <tuple>
              | <structure>
              | <function>
              | <array>
              | <named_type>

<type_def>  ::= <type> <declarator> {"," <declarator>}
              | <enum_def>
              | <sort_def>

Semantics

1.: (Type) A Type (<type>) is a (possibly empty⁹, possibly infinite) set of values. For example, the Boolean type bool is the set false,true}.
2.: (TypeDef) <type_def> is a type definition (or a definition of a named type) that associates an identifier <id> to a type. The identifier can be used, as part of a <path_id>, wherever a <type> is expected. If a type is defined using a <declarator>, then it is the first <id> of that <declarator> that is being defined.
3.: (TypeIdSpace) The identifier of a type resides in the namespace of types, and is visible everywhere in its scope, regardless of the position of the <type_def>.
4.: (TypeCalc) The resulting type associated to the identifier being defined by a type definition (a <type_def>) involving a <type> (the base type) and a <declarator> is calculated according to procedure calc_type in Section 7.
5.: (InlineMultTypeDef) A single type definition <type> D₁,D₂,…D_n where each D_i is a <declarator> is equivalent to n type definitions <type> D₁, <type> D₂, …<type> D_n.
6.: (TypeCompatibility) The Compatibility relation C(T₁,T₂) between types is an equivalence relation (reflexive, symmetric and transitive) defined in the remainder of the document. Two types are said to be Compatible iff C(T₁,T₂) = true. In Section 10.4 we will extend this relation to include domains (<domain>).
7.: (TypeAssignability) The Assignability relation A(T₁,T₂) between types is a preorder (reflexive and transitive) defined in the remainder of the document. A type T₁ is said to be Assignable to another type T₂ iff A(T₁,T₂) = true.

Restrictions

1.: (TypeDefUnicity) A named type which is defined by a <type_def> which is not a <sort_def> may only be defined once per scope of the namespace of types.
2.: (TypeDefCausality) A named type may not be defined in terms of itself, either directly or indirectly. This restriction also applies to sort contributions: a sort may not contribute to its own definition.

8.1 Scalar Types

Scalar Types are the subset of HLL types that consists of scalar (or atomic) values. These are the Boolean, integer, enum and sort types.

8.1.1 Boolean Type

Syntax

Semantics

1.: (BoolValues) The type bool is comprised of the two values true and false.
2.: (BoolCompatibility) The bool type is compatible with itself.
3.: (BoolAssignability) The bool type is assignable to itself.
4.: (BoolValueOrder) false < true.

Restrictions

8.1.2 Integer Types

HLL’s integer types can be either finite or infinite (the set ℤ). Finite types are restricted by either an inclusive range (for example int [4, 9]), or an “implementation” (for example int signed 32). Historically, the main purpose of finite integer types has been to give bounds to inputs (free variables) and state-holding elements (latches and pre-expressions), thus ensuring that the state-space of an HLL system is finite. However, since HLL version 3.0, all stream variables declared with a finite integer type T will in each time step only take values from T, except on overflow which will result in nil being taken instead.

Syntax

(IntSyntax)

<integer>   ::= "int"
              | "int" <sign>
              | "int" <range>
<sign>      ::= "signed" <id_or_int>
              | "unsigned" <id_or_int>
<id_or_int> ::= <id>
              | <int_literal>
<range>     ::= "[" <expr> "," <expr> "]"

Forward References

1.: <expr> is defined in Section 10.

Semantics

1.: (IntValues) The type int is comprised of all integers (the set ℤ).
2.: (IntSignedValues) The type int signed E₁ is comprised of the integers in the interval [−2^E₁−1,2^E₁−1 −1].
3.: (IntUnsignedValues) The type int unsigned E₂ is comprised of the integers in the interval [0,2^E₂ −1].
4.: (IdOrInt) <id_or_int> is a constant stream expression restricted to integer constants (<id>) and integer literals (<int_literal>).
5.: (IntRangeValues) The type int [E₃,E₄] is comprised of the integers in the interval [E₃,E₄].
6.: (IntCompatibility) All integer types are compatible with each other.
7.: (IntAssignability) All integer types are assignable to each other.
8.: (IntValueOrder) i < i + 1 for any integer i.

Restrictions

1.: (IntSizeInteger) E₁,E₂,E₃ and E₄ shall be of integer type.
2.: (IntSizeConstant) 𝒮ℱ(E_i) = 2 for i ∈ [1,4].
3.: (SignedBitsPositive) E₁ > 0.
4.: (UnsignedBitsNonNegative) E₂ ≥ 0.
5.: (IntSizeNotNil) Mint(E_i,k)≠nil for i ∈ [1,4] and all k.

Related Notation

1.: The types int <sign> are called Integer implementation types.
2.: The types int <range> are called Integer range types.

8.1.3 Enum Types

Syntax

(EnumSyntax)

<enum_def>   ::= <enumerated> <id>
<enumerated> ::= "enum" "{" <id_list> "}"

Semantics

1.: (EnumDef) The enum type defined as enum {V₁,V₂,…V_n} is comprised of the values {V₁,V₂,…V_n}.
2.: (EnumValueSpace) The values of an enum type reside in the namespace of streams.
3.: (EnumValueDef) The definition of an enum type also defines its values.
4.: (EnumCompatibility) An enum type is compatible with itself.
5.: (EnumAssignability) An enum type is assignable to itself.
6.: (EnumValueOrder) V_i < V_i+1.

Static Flag

1.: (EnumValueStaticFlag) 𝒮ℱ(V) = 2 for an enum value V.

Restrictions

1.: (EnumValueUnicity) An enum value may not be defined more than once per scope of the namespace of streams.

8.1.4 Sort Types

Syntax

(SortSyntax)

<sort_def>     ::= "sort" [ <sort_contrib> "<" ] <id>
<sort_contrib> ::= <path_id_list>
                 | "{" <id_list> "}"
<path_id_list> ::= <path_id> {"," <path_id>}

Semantics

1.: (SortDef) A <sort_def> is a contribution to the definition of a sort type. A <sort_def> without a <sort_contrib> is an empty contribution to the sort type. (The name of the sort type is given by the <id> as in any type definition.)
2.: (SortContrib) A sort type is defined by one or more contributions. The values of the sort type is the union of the values of its contributions.
3.: (SortContribScope) Contributions to a sort type S can only be made within the same scope.¹⁰
4.: (SortValueSpace) The values of a sort type reside in the namespace of streams.
5.: (SortSubTypeContrib) sort S₁,S₂,…S_k < S denotes the contribution of sort types S₁,S₂,…S_k to sort type S, and the inclusion of their values into S (i.e. S₁ ∪S₂ ∪…∪S_k ⊆ S).
6.: (SortValueContrib) sort {V₁,V₂,…V_n} < S denotes the definition of the values V₁,V₂,…V_n, and their inclusion into the sort type S (i.e. {V₁,V₂,…V_n}⊆ S).
7.: (SortCompatibility) All sort types are compatible with each other.
8.: (SortAssignability) A sort type T₁ is assignable to another sort type T₂ if either T₁ is the same type as T₂, or T₁ contributes, either directly or indirectly, to the definition of T₂.
9.: (SortValueOrder) Not defined.

Static Flag

1.: (SortValueStaticFlag) 𝒮ℱ(V) = 2 for a sort value V.

Restrictions

1.: (SortValueUnicity) A sort value may not be defined more than once per scope of the namespace of streams.
2.: (SortSubTypes) S_i for i ∈ [1,k] of (SortSubTypeContrib) shall refer to sort types.

¹⁰Two different sort types named S are defined in the following example. One is defined on the global top-level and one within the user namespace N:

8.2 Composite Types

Composite Types are the subset of HLL types that are not scalar. A composite type is a composition of HLL types, with each type of the composition said to be a Component of the composite type. By extension, a stream of composite type is made up by components, which are themselves streams. The composite types are tuples, structs, arrays, and functions.

8.2.1 Tuple Types

A tuple type tuple {bool, int [0, 2]} consists of the 2 ∗ 3 = 6 values in the set bool×int [0,2], i.e. {(false,0),(false,1),(false,2),(true,0),(true,1),(true,2)}.

Syntax

(TupleSyntax)

<tuple> ::= "tuple" "{" <type_list> "}"

Semantics

1.: (TupleType) A tuple is a composition of ordered unnamed components. The components are ordered according to the order they appear in the text.
2.: (TupleValues) The type tuple {T₁,T₂,…T_n} is comprised of the values in the n-fold Cartesian product of its component types, i.e. the set T₁ ×T₂ ×…×T_n.
3.: (TupleCompatibility) Two tuple types are compatible iff they have the same number of components and the types of those components are pair-wise compatible.
4.: (TupleAssignability) A tuple type T₁ is assignable to another tuple type T₂ iff they have the same number of components and each component of T₁ is assignable to its corresponding component in T₂.

Restrictions

Related Notation

1.: Given a value V_T of tuple type tuple {T₁,T₂,…T_n} and an integer literal K with 0 ≤ K < n, we will write V_T@K to denote the component of V_T of type T_K+1 at the 0-based index K. Note that @ is an operation on tuple values, and distinct from the HLL tuple accessor (.K) that operates on tuple streams.

8.2.2 Struct Types

From a user’s perspective, the only difference between a struct and a tuple is the way to access the components: struct components are accessed by their names, whereas tuple components are accessed using a 0-based integer index. The two types are nevertheless distinct and cannot be mixed.

Syntax

(StructSyntax)

<structure>   ::= "struct" "{" <member_list> "}"

<member_list> ::= <id> ":" <type> {"," <id> ":" <type>}

Semantics

1.: (StructType) A struct is a composition of ordered named components. The components are ordered according to the order they appear in the text.
2.: (StructValues) The type struct {M₁ : T₁,M₂ : T₂,…M_n : T_n} is comprised of the same values as the corresponding tuple type tuple {T₁,T₂,…T_n} (see (TupleValues)).
3.: (StructCompIdSpace) The identifiers of the components reside together in their own namespace. (One can see this as the struct type introducing a new namespace to which the named components belong. This means that two struct types may have components with the same name without any clash, even if one is nested within the other.)
4.: (StructCompatibility) Two struct types are compatible iff they have the same number of components and the types of those components are pair-wise compatible and the names of those components pair-wise equal.
5.: (StructAssignability) A struct type T₁ is assignable to another struct type T₂ iff they have the same number of components and each component of T₁ has the same name as, and is assignable to, its corresponding¹¹ component in T₂.

Restrictions

1.: (StructCompUnicity) Two components of the same struct type may not have the same name.

Related Notation

1.: Given a value V_S of struct type struct {M₁ : T₁,M₂ : T₂,…M_n : T_n} and an identifier M_i with 1 ≤ i ≤ n, we will write V_S@M_i to denote the component of V_S of type T_i with the name M_i. Note that @ is an operation on struct values, and distinct from the HLL struct accessor (.M) that operates on struct streams.

¹¹Corresponding means here “at the same position” (the components of struct types are ordered).

8.2.3 Function Types

A function type (int [0, 2] -> bool) consists of the three components (of type bool) corresponding to the inputs 0, 1 and 2. The type consists of the 2³ = 8 values in the set bool^|int[0,2]|, i.e. {(false,false,false), (false,false,true), (false,true,false), (false,true,true), (true,false,false), (true,false,true), (true,true,false), (true,true,true)}.

This example of a function type adopts the point of view that the function is a composite object (much like an array) consisting of three components. However, there is also the alternative point of view of a function as a mapping between two sets; the domain and the range (or image). Seeing our example above from this point of view, we will identify the domain with the set {0,1,2} and the range with the set {false,true}. A function value is thus equivalent to a mapping from a value of the function’s domain to a value of the function’s range¹² . For example the function value (false,true,true) from the example above corresponds to the mapping 0

false,1

true,2

true.

We note that in the “object view” of a function type, the components have to be ordered in a way that allows us to find the component value corresponding to a given input value, whereas in the “mapping view” such an order is not needed. Since function values expressed as n-tuples is a completely abstract concept and not related to any HLL operation, it means that for the “object view” of function types, any order of the components will work as long as it is consistently used. That being said, some concrete HLL operations such as the definition of a function using a collection on the right hand side, written as f := {false, true, true}; and defined in Section 12, do require that a known order is defined for the function components. This order is defined by (FunctionCompOrder) on the next page, and is only defined for ordered domain types (thus excluding functions of sort domain).

Since a function value is a mapping from a value (of the function’s domain) to a value (of the function’s range), it would be natural to assume that a stream of function values is a mapping from a stream to a stream. This is not the case however, and may be a source of confusion. An HLL function is a stream of combinatorial functions (i.e. mappings from values to values) and not a function on streams, which means it is not possible to use HLL functions to express temporal functions (i.e. functions which talk about the past or future values of their stream parameters). HLL functions are characterized by the following property:

for each time step k, x = y -> f(x) = f(y), regardless of the history (past or future values) of x and y.

Expressions such as f(x) (which are introduced in Section 10.6) where both f and x are streams, should thus be understood as the point-wise application of the value of f on the value of x in each time step:

f :    f₀     f₁     f₂     …     f_n     …
x :    x₀     x₁     x₂     …     x_n     …
f(x) :    f₀(x₀)     f₁(x₁)     f₂(x₂)     …     f_n(x_n)     …

Syntax

(FunctionSyntax)

<function> ::= "(" <type> {"*" <type>} "->" <type> ")"

Semantics

1.

(FunctionType) A function is a composition of unnamed components, which are all of the same Return type.

2.

(FunctionValues) A function type (T₁ ∗T₂ ∗…∗T_n -> T) consists of:

(a): Parameter types T₁ to T_n. The set T₁ ×…×T_n is also called the function’s Domain.
(b): A return type (or component type) T. The set T is also called the function’s Range.

The function type is comprised of the values in the Cartesian power T^{|T₁×T₂×…×T_n|} (alternatively written as the Cartesian product ∏ _{i∈T₁×T₂×…×T_n}T.)

If n > 1 then the function type is said to be Multivariate.

3.

(FunctionCompOrder) The components of a function are ordered iff the parameter types are ordered, i.e. iff they each have an order defined on their values. In that case the order of the components is the same as the order of the parameter types’ values, where the first parameter type is the most significant one.

4.

(FunctionDomainEquality) Two function parameter types T₁ and T₂ are said to be equal iff they are mutually assignable to each other and their sets of values are equal, i.e. v ∈ T₁ ↔ v ∈ T₂.¹³

5.

(FunctionCompatibility) Two function types are compatible iff they have the same number of parameter types and those are all pair-wise equal according to (FunctionDomainEquality), and their return types are compatible.

6.

(FunctionAssignability) A function type (T₁ ∗T₂…∗T_n -> T) is assignable to another function type (U₁ ∗U₂…∗U_n -> U) iff T_i is equal to U_i (according to (FunctionDomainEquality)) for i ∈ [1,n] and T is assignable to U.

Restrictions

1.: (FunctionDomainScalar) The parameter types T_i for i ∈ [1,n] of a function type (T₁ ∗T₂ ∗…∗T_n -> T) shall be of scalar type.

Related Notation

1.: Given a value V_F of function type (T₁ ∗T₂ ∗…∗T_n -> T) and values V_i with V_i ∈ T_i, we will write V_F(V₁,V₂,…V_n)_V to denote the component (or output) value of V_F of type T corresponding to the inputs V₁,V₂,…V_n. We employ a subscript V on the right parenthesis ()_V) in order to emphasize that this is an operation on function values, and distinct from the HLL function accessor that operates on function streams. Of course, the subscript V is not strictly necessary since function values are functions in the mathematical sense (mappings from values to values) and the operation ()_v corresponds thus to the usual function application in the mathematical sense.

8.2.4 Array Types

An array type bool^(3) (an array of 3 bool) is equivalent to the function type
(int [0, 2] -> bool), except for the way to access the components (A[0] vs A(0)).

Syntax

(ArraySyntax)

<array> ::= <type> "^" "(" <expr_list> ")"

Semantics

1.: (ArrayType) An array is a composition of ordered unnamed components, which are all of the same Base type.
2.: (ArrayValues) The type T (E₁,E₂,…E_n) is equivalent to¹⁴ the function type (int [0,E₁ −1] ∗int [0,E₂ −1] ∗…∗int [0,E_n −1] -> T), except for the way to access the components. T is the base type (the component type) of the array and the E_i are called the Dimensions of the array and if n > 1 then the array type is said to be Multidimensional.
3.: (ArrayCompatibility) An array type T₁ (D₁,D₂,…D_n) is compatible with another array type T₂ (E₁,E₂,…E_n) if each D_i = E_i and T₁ is compatible with T₂.
4.: (ArrayAssignability) An array type T₁ (D₁,D₂,…D_n) is assignable to another array type T₂ (E₁,E₂,…E_n) if each D_i = E_i and T₁ is assignable to T₂.

Restrictions

1.: (ArrayDimConstant) 𝒮ℱ(E_i) = 2 for i ∈ [1,n].
2.: (ArrayDimNotNil) Mint(E_i,k)≠nil for i ∈ [1,n] and all k.

Related Notation

1.: Given a value V_A of array type T (E₁,E₂,…E_n), and values V_i with 0 ≤ V_i < E_i of integer type, we will write V_A[V₁,V₂,…V_n]_V to denote the component of V_A of type T at index V₁,V₂,…V_n. We employ a subscript V on the right square bracket (]_V) in order to emphasize that this is an operation on array values, and distinct from the HLL array accessor that operates on array streams.

¹⁴This means that it is possible to consistently replace all array types by equivalent function types (while changing all accesses from [i₁,…i_n] to (i₁,…i_n)) in an HLL text. However, array and function types are still not compatible with or assignable to each other as specified by (ArrayCompatibility) and (ArrayAssignability).

8.3 Named Types

Syntax

Semantics

1.: (NamedType) A named type (<named_type>) is the type that it refers to.
2.: (NamedTypeCompatibility) A named type is compatible with the type it refers to.
3.: (NamedTypeAssignability) A named type is mutually assignable with the type it refers to.

Restrictions

1.: (NamedTypeRef) The <path_id> of a <named_type> shall refer to an existing type (in the namespace of types).

8.4 Implicit Types

Implicit types have no explicit syntax, but can appear implicitly as a result of some other syntactic construct of the language. For example a <collection> {false, 0} has a collection type, and an <ite_expr> if E₁ then E₂ else E₃ has a type which is the union of the types of E₂ and E₃.

8.4.1 Collection Types

A collection {false, 0} (a <collection>, defined in Section 12) is assignable to a variable declared with, for example, type tuple {bool, int} or struct {b: bool, i:int}. A collection {false, true, false} is assignable to a variable V declared, for example, using one of the following declarations:

Syntax

Semantics

1.: (CollectionReason) A collection type is the type associated with collections (<collection>, see Section 12).
2.: (CollectionType) The type of {R₁,R₂,…R_n} where R_i is of type T_i is the collection type {T₁,T₂,…T_n}, composed of n ordered components. We will count the collection types among the composite types of HLL.
3.: (CollTupleCompatibility) A collection type T₁ is compatible with a tuple type T₂ iff they have the same number of components and each component of T₁ is compatible to its corresponding component in T₂.
4.: (CollTupleStructAssignability) A collection type T₁ is assignable to a tuple or struct type T₂ iff they have the same number of components and each component of T₁ is assignable to its corresponding component in T₂.
5.: (CollArrayAssignability) A collection type T₁ is assignable to an array type T₂ (E) iff T₁ has E components and each one is assignable to T₂.
6.: (CollMultiDimArrayAssignability) A collection type T₁ is assignable to a multidimensional array type T₂ (E₁,E₂,…E_n) (n > 1) iff T₁ has E₁ components and each one is assignable to T₂ (E₂,…E_n).
7.: (CollFuncAssignability) A collection type T₁ is assignable to a function type (T₂ -> T₃) iff T₂ is an ordered type and T₁ has |T₂| components and each one is assignable to T₃.
8.: (CollMultiVarFuncAssignability) A collection type T₁ is assignable to a multivariate function type (T₂ ∗T₃ ∗…∗T_n−1 -> T_n) (n > 3) iff T₂ is an ordered type and T₁ has |T₂| components and each one is assignable to (T₃ ∗…∗T_n−1 -> T_n).

Restrictions

8.4.2 Unsized Types

In HLL, it is possible to restrict the set of values of integer inputs and memories, as well as other declared stream variables, either by using a “range” (e.g. int [0, 7]) or an “implementation” (e.g. int unsigned 3). However, for arbitrary integer expressions, the only type used is int without restriction. The Unsized copy of a type (defined below) is used to remove its size restriction in certain cases, for example when computing the union type of the two branches of an if-then-else (see Sections 8.4.3 and 10.1).

Syntax

Semantics

1.: (UnsizedInteger) The unsized copy of an integer type T is the type int.
2.: (UnsizedScalar) The unsized copy of a non-integer scalar type T is T.
3.: (UnsizedComposite) The unsized copy of a composite type T is a type T’, in all respects the same as T, but with each component type replaced by its unsized copy.¹⁵

Restrictions

¹⁵To give two examples, the unsized copy of tuple {int signed E₁,int [E₂,E₃]} is tuple {int,int}, and the unsized copy of (int [E₁,E₂] -> int [E₃,E₄]) is (int [E₁,E₂] -> int).

8.4.3 Union Types

Syntax

Semantics

1.: (UnionScalar) The union type of n compatible non-sort scalar types T₁…T_n is the unsized copy of T₁.
2.: (UnionSort) The union type of n sort or sort union types T₁…T_n (i.e. each T_i may be either a sort type or another sort union type) is a special “sort union type” T_u. We will count the sort union type among the scalar types of HLL.
3.: (UnionComposite) The union type of n compatible composite types T₁…T_n, which are not collection types, is a type T_r, in all respects the same as any of the T_i, but where each component type of T_r is the union type of the n corresponding component types of T₁…T_n.
4.: (UnionTupleCollection) The union type of a tuple type T₁ and a compatible collection type T₂ is a tuple type T_r, in all respects the same as T₁, but where each component type of T_r is the union type of the corresponding component types of T₁ and T₂. This union is needed to represent the type of SELECT expressions where the default value is a collection, see (QuantSelectType).
5.: (SortUnionCompatibility) A sort union type is compatible with both sort types and other sort union types.
6.: (SortUnionAssignability) A sort union type T_u of the types T₁…T_n is assignable to a sort type T_s iff each T_i for i ∈ [1,n] is assignable to T_s.¹⁶

Restrictions

¹⁶Note that this definition relies on a recursion, since the T_i may themselves be sort unions. The recursion is well-founded since at the base case level we only have sort types.

9 Accessors

Syntax

(AccessorSyntax)

<accessor> ::= "." <id>
             | "." <int_literal>
             | "[" <expr_list> "]"
             | "(" [<expr_list>] ")"

Forward References

1.: <int_literal> is defined in Section 10.7.2.

Semantics

1.: (AccStruct) .M (an <id>) designates a struct component named M.
2.: (AccTuple) .N (an <int_literal>) designates the (N+1):th component of a tuple (the indexing is 0-based).
3.: (AccArray) At time step k and relative to an array type T (D₁,D₂,…D_n), [E₁, E₂,…E_n] designates the array component of type T at the index given by [Mint(E₁,k),Mint(E₂,k),…Mint(E_n,k)]_V, or if there is no such component (the index is out of bounds or nil), it designates nil.
4.: (AccFunction) At time step k and relative to a function type (T₁ ∗T₂ ∗…∗T_n -> T_r), (E₁, E₂,…E_n) designates the function output of type T_r corresponding to the inputs (M_T₁(E₁,k),M_T₂(E₂,k),…M_{T_n}(E_n,k))_V, or if there is no such output (some input is out of the function domain or nil), it designates nil.

Restrictions

1.: (ArrayIndexInteger) Each E_i of an accessor [E₁, E₂,…E_n] shall be of integer type.
2.: (FunctionInputScalar) Each E_i of an accessor (E₁, E₂,…E_n) shall be of scalar type.

10 Expressions

Syntax

(ExprSyntax)

<expr>          ::= <ite_expr>
                  | <lambda_expr>
                  | <binop_expr>
                  | <membership_expr>
                  | <unop_expr>
                  | <proj_expr>

Semantics

1.

(Expr) An Expression E (an <expr>) is a stream (of values) of some type T.

2.

(EmptyScalarTypeNil) If some scalar component of T (or T itself) is an empty scalar type, then the corresponding component of a stream expression E (or E itself) of type T will carry the value nil in each time step.

3.

(ExprPrecedence) The precedence of expressions is given below in order from lowest to highest (same line means same precedence):

(a): <ite_expr>, <lambda_expr>
(b): <binop_expr>, <membership_expr>
(c): <unop_expr>
(d): <proj_expr>

Restrictions

Related Notation

1.: We will write E<V₁ := R₁,V₂ := R₂,…V_n := R_n> to denote substitution, i.e. the process of replacing all free occurrences of the variables V₁,V₂,…V_n in the expression E with expressions R₁,R₂,…R_n.
As an example (x + y = z)<z := 5> is equivalent to x + y = 5. By contrast, (SOME z : [0,4] (x + y = z))<z := 5> is equivalent to SOME z : [0,4] (x + y = z) (no substitution performed) since the quantifier variable z is not free in this case (it is bound by the quantification).

10.1 If-Then-Else Expressions

Syntax

(IteExprSyntax)

<ite_expr> ::= "if"   <expr> "then" <expr>
              {"elif" <expr> "then" <expr>}
               "else" <expr>

Semantics

1.

(Elif) elif is equivalent to else if.

2.

(IfThenElse) In each time step, if E₁ then E₂ else E₃ evaluates to 1) nil if E₁ is nil, 2) E₂ if E₁ is true and 3) E₃, otherwise (E₁ is false). The type T of the expression is the union type of the type T₂ of E₂ and the type T₃ of E₃. Formally:

MT(if E₁ then E₂ else E₃,k) =

( { nil if Mbool(E1,k) = nil = ( MT2(E2,k) if Mbool(E1,k) = true MT3(E3,k) otherwise (Mbool (E1,k) = false)

Static Flag

1.: (IteExprStaticFlag)
𝒮ℱ(if E₁ then E₂ else E₃) = min(𝒮ℱ(E₁),𝒮ℱ(E₂),𝒮ℱ(E₃)).

Restrictions

1.: (IteCondBool) The type of E₁ shall be bool.
2.: (IteBranchesCompatible) The types of E₂ and E₃ shall be compatible.

10.2 Lambda Expressions

Lambda expressions can be used to build unnamed streams of array or function type. For example “lambda[3]:[i] := i = 1” is an array of the 3 Boolean constants false (at index 0), true (at index 1), false (at index 2).

Lambda expressions can, together with a definition, be used to build recursive array or function definitions. As an example, the Fibonacci numbers are calculated by a recursion below (all proof obligations are valid).

Allowing recursion in this manner provides HLL with a powerful tool, but unfortunately it also means that it becomes possible to express undecidable problems in HLL, since it is possible to build recursions that do not terminate. Whether or not a recursion will terminate depends on the reasoning power of tools implementing HLL, and is thus outside the scope of this document.

A specificity of lambda expressions is how their type is computed. Two lambda expressions which at a glance may look as if of different type, may in fact be of the same type. The type of a lambda expression is computed according to (LambdaType) on the next page. In the following example, the two lambda expressions that are being compared are of the same type (the type int (3) (4)), and the proof obligation is valid.

Lambda expressions are – just as any HLL function (or array) as discussed in Section 8.2.3 – streams of combinatorial functions (mappings from values to values). The formal definition of lambda arrays and functions (in (LambdaArray) and (LambdaFunction) below) defines, for a given time step k, one such combinatorial function. The combinatorial function takes as inputs the values V₁ to V_n and returns:

¹⁷lambda[1] : [i] := (lambda[1] : [i] := i) is not reducible to lambda[1][1] : [i][i] := i (since the latter expression is not legal), so the two are not equivalent.

Syntax

(LambdaExprSyntax)

<lambda_expr> ::= "lambda" {<declarator_suffix>}+ ":"
                  {<formal_param>}+ ":=" <expr>

<formal_param>  ::= "[" <id_list> "]"
                  | "(" <id_list> ")"

Semantics

1.

(LambdaScope) A <lambda_expr> introduces a local scope in the namespace of streams, called a Lambda scope that starts at the "lambda" keyword and continues to the end of the expression. Parameters (<formal_param>) declared within the scope must be unique, but can hide other variables or parameters above it.

2.

(LambdaType) The type T of a lambda expression lambda DS : FP := E where E is an expression of type T₁ is equal to calc_type(T₂,DS), where the type T₂ is calculated by solving the following equation: T₁ = calc_type(T₂,DS_suffix) where DS_suffix is the N last elements of the list DS where N is the difference in length of the list DS and the list FP, i.e. N = |DS|−|FP|. The function calc_type is defined in Section 7.

Note that if the length of the lists DS and FP is the same (i.e. N = 0), then DS_suffix = {} (the empty list) and T₁ = T₂.

3.

(LambdaMultFormalParam) lambda D₁…D_n : P₁…P_n:= E is reducible¹⁷ to lambda D₁…D_n−1 : P₁…P_n−1:= (lambda D_n : P_n:= E).

4.

(LambdaDeclSuffixOverhang) lambda D₁…D_n : P₁…P_k:= E with n > k is (if well-typed) equivalent to lambda D₁…D_k : P₁…P_k:= E.

5.

(LambdaArray) lambda[E₁,…E_n] : [i₁,…i_n]:= E, where E is of type T_E, and i_j for j ∈ [1,n] is, by definition, of type int, is an expression of type T_E (E₁,…E_n) such that:

M_{T_E (E₁,…E_n)}(lambda[E₁,…E_n] : [i₁,…i_n]:= E,k)[V₁,…V_n]_V =

{ MTE(E<i1:= V1,...in:= Vn>,k) if ∀j ∈ [1,n] : 0 ≤ Vj < Ej = nil otherwise

(Note that the values V₁ to V_n are implicitly converted to constant streams before they are substituted for the formal parameters i₁ to i_n.)

6.

(LambdaFunction) lambda(T₁,…T_n) : (i₁,…i_n):= E, where E is of type T_E, and i_j for j ∈ [1,n] is, by definition, of type T_j, is an expression of type (T₁ ∗…∗T_n -> T_E) such that:

M_{(T₁∗…∗T_n -> T_E)}(lambda(T₁,…T_n) : (i₁,…i_n):= E,k)(V₁,…V_n)_V =

{ = MTE(E<i1:= V1,...in:= Vn>,k) if ∀j ∈ [1,n] : Vj ∈ Tj nil otherwise

(Note that the values V₁ to V_n are implicitly converted to constant streams before they are substituted for the formal parameters i₁ to i_n.)

Static Flag

1.: (LambdaStaticFlag) 𝒮ℱ(<lambda_expr>) = 0.
2.: (FormalParamStaticFlag) 𝒮ℱ(i) = 1 for a lambda parameter i (e.g. lambda[1] : [i] := <expr>).

Restrictions

1.: (LambdaParamUnicity) Two parameters of a lambda expression may not have the same name.
2.: (LambdaParamsBound) |DS|≥|FP| (the number of elements of the list DS shall be greater than or equal to the number of elements of the list FP) for an expression lambda DS : FP := E.
3.: (LambdaParamsMatch) Each element F (a <formal_param>) of the list FP in an expression lambda DS : FP := E, where F itself is a list (an <id_list>), shall contain the same number of elements (of form <id>) as the element D (a <declarator_suffix> and itself a list; either an <expr_list> or a <type_list) of the corresponding position in the list DS.
Furthermore, if D is on the form "[" <expr_list> "]" then F shall be on the form "[" <id_list> "]", and if D is on the form "(" <type_list> ")" then F shall be on the form "(" <id_list> ")".
4.: (LambdaTypeCheck) There shall be exactly one solution to the equation T₁ = calc_type(T₂,DS_suffix) of (LambdaType).

10.3 Binop Expressions

Syntax

(BinopSyntax)

<binop_expr> ::= <expr> <binop> <expr>
<binop>      ::= "#" | "&"  | "#!" | "->" | "<->"
               | ">" | ">=" | "<"  | "<="
               | "=" | "==" | "!=" | "<>"
               | "+" | "-"  | "*"  | "^" | "<<" | ">>"
               | "/" | "/>" | "/<" | "%"

Semantics

1.

(BoolAnd) E₁ & E₂ (Boolean and) is equivalent to ~(~E₁ # ~E₂) (De Morgan’s law).

2.

(BoolXor) E₁ #! E₂ (Boolean exclusive or) is equivalent to ~(E₁ <-> E₂).

3.

(BoolImpl) E₁ -> E₂ (Boolean implication) is equivalent to ~E₁ # E₂.

4.

(BoolEquiv) E₁ <-> E₂ (Boolean equivalence) is reducible to E₁ = E₂.

5.

(IntGt) E₁ > E₂ (greater than) is equivalent to E₂ < E₁.

6.

(IntGte) E₁ >= E₂ (greater than or equal to) is equivalent to ~(E₁ < E₂).

7.

(IntLte) E₁ <= E₂ (less than or equal to) is equivalent to E₂ >= E₁.

8.

(OpNeq) E₁ != E₂ and E₁ <> E₂ are both equivalent to ~(E₁ = E₂).

9.

(OpEqEq) == is equivalent to =.

10.

(IntSub) E₁ - E₂ (subtraction) is equivalent to E₁ + (-E₂).

11.

(IntLeftShift) E₁ << E₂ (left shift) is reducible to E₁ * (2 E₂).

12.

(IntRightShift) E₁ >> E₂ (right shift) is reducible to E₁ /> (2 E₂).

13.

(IntFloorDiv) E₁ /> E₂ (floor division) represents the biggest integer smaller than or equal to the rational E₁∕E₂. Formally, it is equivalent to:

if (E₁ < 0) = (E₂ < 0) # E₁ % E₂ = 0 then E₁ / E₂ else E₁ / E₂ - 1

14.

(IntCeilDiv) E₁ /< E₂ (ceiling division) represents the smallest integer bigger than or equal to the rational E₁∕E₂. Formally, it is equivalent to:

if (E₁ < 0) = (E₂ < 0) & E₁ % E₂ != 0 then E₁ / E₂ + 1 else E₁ / E₂

15.

(IntRem) E₁ % E₂ (remainder) is equivalent to E₁ - (E₁ / E₂) * E₂.

Core Constructs:

16.

(BoolOr) E₁ # E₂ (Boolean or) is a stream of type bool for which Mbool(E₁ # E₂,n) = Mbool(E₁,n) ∨_nilMbool(E₂,n) holds. The operator ∨_nil is the usual Boolean OR operator extended to three-valued logic according to the following table:


A ∨_nilB		B

		false	nil	true


	false	false	nil	true

A	nil	nil	nil	true

	true	true	true	true

17.

(IntLt) E₁ < E₂ (less than) is a stream of type bool for which Mbool(E₁ < E₂,n) = Mint(E₁,n) < _nilMint(E₂,n) holds. The operator < _nil is the usual “strictly less than” comparison operator defined on integers, and extended for the nil case according to the following table:


A < _nilB		B

		nil	Y


A	nil	nil	nil

	X	nil	X < Y

18.

(IntAdd) E₁ + E₂ (addition) is a stream of type int for which Mint(E₁ + E₂,n) = Mint(E₁,n) + _nilMint(E₂,n) holds. The operator +_nil is the usual integer addition operator extended for the nil case according to the following table:


A + _nilB		B

		nil	Y


A	nil	nil	nil

	X	nil	X + Y

19.

(IntMul) E₁ * E₂ (multiplication) is a stream of type int for which Mint(E₁ * E₂,n) = Mint(E₁,n) ∗_nilMint(E₂,n) holds. The operator ∗_nil is the usual integer multiplication operator extended for the nil case according to the following table:


A ∗_nilB		B

		nil	Y


A	nil	nil	nil

	X	nil	X ∗ Y

20.

(IntDiv) E₁ / E₂ (integer division) is a stream of type int for which Mint(E₁ / E₂,n) = Mint(E₁,n)∕_nilMint(E₂,n) holds. The operator ∕_nil is the usual integer division operator (this means a truncating division; i.e. division with the fractional part omitted) extended for the nil case according to the following table:


A∕_nilB		B

		0	nil	Y


A	nil	nil	nil	nil

	X	nil	nil	X∕Y

21.

(IntExp) E₁ E₂ (exponentiation) is a stream of type int for which Mint(E₁ E₂,n) = Mint(E₁,n) ˆ_nil Mint(E₂,n) holds. The operator ˆ_nil is defined in the following table:


A ˆ_nil B

		< 0	0	nil	Y


	0	nil	1	nil	0

A	nil	nil	nil	nil	nil

	X		1	nil	X^Y

Note: The division operation refers to integer division, which means that this expression can only take the values −1, 0 or 1.

22.

(OpEqScalar) E₁ = E₂ (scalar equality), where E₁ and E₂ are of scalar compatible types T₁ and T₂, is a stream of type bool for which Mbool(E₁ = E₂,n) = (M_T₁(E₁,n) = _nilM_T₂(E₂,n)) holds. The operator = _nil is the usual equality operator extended for the nil case according to the following table:


A = _nilB		B

		nil	Y


A	nil	nil	nil

	X	nil	X = Y

23.

(OpEqCompositeUniDim) E₁ = E₂ (composite unidimensional equality), where E₁ and E₂ are of composite compatible types T_E₁ and T_E₂, which are neither multidimensional array types nor multivariate function types, is equivalent to:

\text{[math]}

where:

\text{[math]}

24.

(OpEqCompositeMultiDim) E₁ = E₂ (composite multidimensional equality), where E₁ and E₂ are of composite compatible types T_E₁ and T_E₂, which are either multidimensional array types or multivariate function types, is equivalent to:

E₁A_0…00 = E₂A_0…00 & … & E₁A_{0…0m_k} = E₂A_{0…0m_k} &

E₁A_0…10 = E₂A_0…10 & … & E₁A_{0…1m_k} = E₂A_{0…1m_k} &

E₁A_{0…m_k−10} = E₂A_{0…m_k−10} & … & E₁A_{0…m_k−1m_k} = E₂A_{0…m_k−1m_k} &

E₁A_m₁m₂…0 = E₂A_m₁m₂…0 & … & E₁A_{m₁m₂…m_k} = E₂A_{m₁m₂…m_k}

where:

A_{i₁…i_k} =

\text{[math]}

Precedence and Associativity:

25.

(BinopGrouping) The precedence of the operators is given below in order from lowest to highest, together with their associativity. Same line means same precedence.

Precedence	Associativity
<-> #!	left
->	right
#	left
&	left
> >= < <= = == != <>	left
<< >>	left
+ -	left
* / /< /> %	left
^	right

Static Flag

1.: (BinopStaticFlag) 𝒮ℱ(E₁ <binop> E₂) = min(𝒮ℱ(E₁),𝒮ℱ(E₂)).

Restrictions

1.: (BoolOrEquivOperandsBool) The operands of # <-> shall be of type bool.
2.: (EqOperandsFiniteCompatible) The operands of = shall be either of compatible scalar types or of compatible composite types with finite numbers of scalar components (either directly or indirectly via other composite components).
3.: (IntCoreBinopOperandsInt) The operands of < + * / ^ shall be of integer type.
4.: (SecondShiftOperandStatic) 𝒮ℱ(E₂) ≥ 1 for an expression E₁ ∘ E₂ with ∘∈{<<, >>}.
5.: (SecondShiftOperandNonNegative) E₂ ≥ 0 for an expression E₁ ∘ E₂ with ∘∈{<<, >>}.

10.4 Membership Expressions

Membership (or elementhood) expressions can be used to test whether the value of some stream expression belongs to a domain, where a domain is a stream of sets of values.

Syntax

(MembershipSyntax)

<membership_expr> ::= <expr> ":" <domain>
<domain>          ::= <range>
                    | <type_domain>
<type_domain>     ::= <named_type>
                    | "bool"
                    | "int"

Semantics

1.: (Domain) A Domain D (<domain>) is a stream of (possibly different) sets of values. We will write D_k to denote the set of values of D at time step k.
2.: (DomainAsType) A <domain> which is a <type_domain> consists in each time step of the set of values of the type T which the <type_domain> refers to. Such a <domain> D is type compatible with the type T.
3.: (DomainAsRange) A <domain> which is a <range> [E₁, E₂] is in each time step k the set of values given by the range [Mint(E₁,k),Mint(E₂,k)]. Such a <domain> is type compatible with the type int. If either of Mint(E₁,k) or Mint(E₂,k) is nil then the <domain> itself is nil at time step k (i.e. we extend the use of the symbol nil to also include domains).
4.: (Membership) E : D, where E is of type T_E, is an expression of type bool such that: $( { nil if MTE(E,k) = nil or Dk = nil Mbool (E : D,k) = ( true if MTE(E,k) ∈ Dk false otherwise$
5.: (MembershipPrecedence) The operator : has the same precedence as the operator =, and is left-associative.

Static Flag

1.: (MembershipStaticFlag) 𝒮ℱ(<membership_expr>) = 0.
2.: (RangeDomainStaticFlag) 𝒮ℱ([E₁, E₂]) = min(𝒮ℱ(E₁),𝒮ℱ(E₂)).
3.: (TypeDomainStaticFlag) The static flag of a <domain> which refers to a type is 2.

Restrictions

1.: (DomainScalar) A <domain> D shall be type compatible with a scalar type.
2.: (MembershipDomainCompatible) The <domain> D of an expression E : D shall be type compatible with the type of E.

10.5 Unop Expressions

Syntax

(UnopSyntax)

<unop_expr> ::= <unop> <expr>
<unop>      ::= "~" | "-"

Semantics

1.: (BoolNeg) ~E (Boolean negation) is nil, true, or false in time step n if E is respectively nil, false or true in time step n. The type of the expression is bool.
2.: (IntNeg) -E (integer negation) is the additive inverse of E (meaning that E + (-E) = 0 holds). The expression is nil in time step n if E is nil in time step n. The type of the expression is int.

Static Flag

1.: (UnopStaticFlag) 𝒮ℱ(<unop> E) = 𝒮ℱ(E).

Restrictions

1.: (BoolNegOperandBool) The operand of ~ shall be of type bool.
2.: (IntNegOperandInt) The operand of - shall be of integer type.

10.6 Projection Expressions

Projection expressions can be used to select components of streams of composite type. For example A[4] selects the array component at index 4, f(true) selects the function component (or output) that corresponds to input true, and so on. An important thing to note is that f(x), where x is an arbitrary stream expression, selects, in time step k, the function output that corresponds to the value of x at time step k, i.e. M(x,k). This means that functions are characterized by the following property:

for each time step k, x = y -> f(x) = f(y), regardless of the history (past or future values) of x and y.

Hence, streams of function type shall be understood as streams of combinatorial functions, and not as functions on streams.

Syntax

(ProjExprSyntax)

<proj_expr> ::= <closed_expr> { <accessor> }

Forward References

1.: <closed_expr> is defined in Section 10.7.

Semantics

1.

(ProjMultipleAcc) A projection expression E A₁ A₂…A_n is equivalent to (…((E A₁) A₂)…) A_n.

2.

(Projection) A projection expression E A where E is a <closed_expr> of composite type T and A an <accessor> compatible with T is equivalent to the component of E designated by A. If A does not designate a valid component¹⁸ of E in time step n, then the expression is equivalent to nil in time step n. Note that the semantics of accessors is detailed in Section 9.

3.

(ProjArrayFunc) This follows directly from Semantic item 4 of Section 9 but is stated again here as a reminder due to its importance: M_T(E(E₁,E₂,…E_n),k) = M_{(T₁∗T₂∗…∗T_n -> T)}(E,k)(M_T₁(E₁,k),M_T₂(E₂,k),… M_{T_n}(E_n,k))_V for all time steps k and types T. (The analogue for array accessors naturally also holds and follows from Semantic item 3 of Section 9.)

To clarify what this entails, then as an example, assume for simplicity that n = 1 and the type of E₁ is comprised of the values in the set {V₁, V₂,…V_n}. Then the expression E(E₁) is equivalent to¹⁹:

if E₁=V₁ then E(V₁) else if E₁=V₂ then E(V₂) else ..
.

if E₁=V_n−1 then E(V_n−1) else E(V_n)

4.

(ProjExprNil) A projection expression E A where E is nil in time step n is also nil in time step n.

Static Flag

1.: (ProjExprStaticFlag) 𝒮ℱ(<proj_expr>) = 0.

Restrictions

1.

(ProjAccCompatible) The accessor A of an expression E A must be compatible with the type T of the expression E, according to the following table:


A	Compatible type T


.K (an <int_literal>)	Tuple with > K components

.M (an <id>)	Struct with a component named M

[E₁, E₂,…E_n]	Array with n dimensions

(E₁, E₂,…E_n)	Function (T₁ ∗T₂ ∗…∗T_n -> T) where
	the type of E_i is assignable to T_i

¹⁹To concretise the example, assume that E is defined with E(i) := ~i & X(i);, then we can use this equivalence to see that E(input) = (if input = true then E(true) else E(false)) = false, and not ~input & X(input).

10.7 Closed Expressions

Closed expressions are a purely syntactic concept, and consist of the explicitly grouped expressions.

Syntax

(ClosedExprSyntax)

<closed_expr> ::= <bool_literal>
                | <int_literal>
                | <named_expr>
                | <next_expr>
                | <pre_expr>
                | <fun_expr>
                | <cast_expr>
                | <with_expr>
                | <case_expr>
                | <quantif_expr>
                | "(" <expr> ")"

Semantics

1.: (GroupedExpr) M((E),n) = M(E,n) for any model M and time step n. (E) has the same type as E. Explicit grouping can be used to override the implicit grouping performed by the parsing of an <expr>. For example (a + b) * c is not equivalent to a + b * c since operator * has a higher precedence than operator +.

Static Flag

1.: (GroupedExprStaticFlag) 𝒮ℱ((E)) = 𝒮ℱ(E).

Restrictions

10.7.1 Boolean Literals

Syntax

(BoolLitSyntax)

<bool_literal> ::= <true> | <false>
<true>         ::= "true"  | "TRUE"  | "True"
<false>        ::= "false" | "FALSE" | "False"

Semantics

1.: (BoolLitTrue) <true> is a stream of type bool such that Mbool(<true>,n) = true for all time steps n.
2.: (BoolLitFalse) <false> is a stream of type bool such that Mbool(<false>,n) = false for all time steps n.

Static Flag

1.: (BoolLitStaticFlag) 𝒮ℱ(<bool_literal>) = 2.

Restrictions

10.7.2 Integer Literals

Syntax

(IntLitSyntax)

<dec_literal> ::= [0-9](_?[0-9])*
<bin_literal> ::= 0[Bb][0-1][_?[0-1])*
<hex_literal> ::= 0[Xx][0-9A-Fa-f](_?[0-9A-Fa-f])*
<int_literal> ::= <dec_literal>
                | <hex_literal>
                | <bin_literal>

Semantics

1.: (IntLitUnderscores) Underscores (_) may be put freely inside integer literals with the purpose of improving readability (for example 1_000_000 or 0xFFFF_FFFF). They can be removed completely without changing the meaning of the literals they appear in, and will not be considered in the following.
2.: (IntLitDecimal) A <dec_literal> shall be intepreted as an integer in base 10 in the standard way (most significant digit first and least significant digit last).
3.: (IntLitBinary) A <bin_literal> starts with the prefix 0B or 0b and is followed by the significant bits. The significant bits shall be interpreted as an unsigned integer in base 2 in the standard way (MSB first and LSB last).
4.: (IntLitHexadecimal) A <hex_literal> starts with the prefix 0X or 0x and is followed by the significant digits. The significant digits shall be interpreted as an unsigned integer in base 16 in the standard way (most significant digit first and least significant digit last).
5.: (IntLiteral) An integer literal <int_literal> with the interpreted value K, as specified above, is a stream of type int such that Mint(<int_literal>,n) = K for all time steps n.

Static Flag

1.: (IntLitStaticFlag) 𝒮ℱ(<int_literal>) = 2.

Restrictions

10.7.3 Named Expressions

Syntax

Semantics

1.: (NamedExpr) If the <path_id> of a <named_expr> refers to an existing stream (in the namespace of streams), then the <named_expr> is that stream.
2.: (NamedExprImplicitDecl) Otherwise, the <named_expr> (which must be unqualified as according to (PathIdNoImplicitDecl)) refers to a unique implicit input stream of type bool. The input stream is implicitly declared by the <named_expr>. The declaration is made in the top-level scope (of the namespace of streams) of the user namespace in which the <named_expr> occurs, or else on the global top-level (if the <named_expr> does not occur inside a user namespace).

Static Flag

1.: (NamedExprStaticFlag) The static flag of a <named_expr> is equal to the static flag of the stream it refers to.
2.: (NamedExprUndefinedStaticFlag) The static flag of an undefined stream variable is 0.

Restrictions

10.7.4 Next Expressions

Syntax

(NextExprSyntax)

<next_expr> ::= "X" "(" <expr> ")"

Semantics

1.: (NextExpr) M(X(E),n) = M(E,n + 1) for any model M and time step n. X(E) has the same type as E.

Static Flag

1.: (NextExprStaticFlag) 𝒮ℱ(<next_expr>) = 0.

Restrictions

10.7.5 Pre Expressions

Syntax

(PreExprSyntax)

<pre_expr> ::= ("pre" | "PRE") ["<" <type> ">"]
               "(" <expr> ["," <expr>] ")"

Semantics

1.: (PreUppercase) PRE is equivalent to pre.
2.: (PreTypedWithInit) pre<T>(E₁,E₂) is an initialized memory stream of type T, where E₂ is the initial value for the initial time step and E₁ is the memorized value for all other time steps. Formally, if T₁ and T₂ correspond respectively to the types of the expressions E₁ and E₂, then the value of the expression at time step k is defined as follows: $( || MT2(E2,0) if value ∈ T ||{ nil otherwise k = 0 MT (pre<T>(E1,E2),k) = |||| MT1(E1,k− 1) if value ∈ T ( nil otherwise k > 0$
3.: (PreTyped) pre<T>(E) is an uninitialized memory stream of type T which takes the value nil in the initial time step. Formally, if T₁ corresponds to the type of the expression E, then the value of the expression at time step k is defined as follows: $( ||{ nil k = 0 MT (pre<T>(E),k) = ||( MT1(E,k− 1) if value ∈ T k > 0 nil otherwise$
4.: (PreUntyped) pre(E) is equivalent to pre<T>(E) where T is the unsized copy (see 8.4.2) of the type of E.
5.: (PreUntypedWithInit) pre(E₁, E₂) is equivalent to pre<T>(E₁, E₂) where T is the union type (see 8.4.3) of the types of E₁ and E₂.

Static Flag

1.: (PreExprStaticFlag) 𝒮ℱ(<pre_expr>) = 0.

Restrictions

1.: (PreOperandsAssignable) The types of the operands E₁ and E₂ of pre<T> (E₁,E₂) and the type of the operand E of pre<T>(E), shall be assignable to T.

10.7.6 Function-Style Expressions

Syntax

(FunopSyntax)

<fun_expr> ::= <fop> "(" <expr_list> ")"
<fop>      ::= "$min"
             | "$max"
             | "$abs"
             | "$or"
             | "$and"
             | "$xor"
             | "$not"
             | "bin2u"
             | "u2bin"
             | "bin2s"
             | "s2bin"
             | "population_count_lt"
             | "population_count_gt"
             | "population_count_eq"

Semantics

1.

(IntMin) $min(E₁, E₂) (minimum) is equivalent to:
(if E₁ < E₂ then E₁ else E₂).

2.

(IntMax) $max(E₁, E₂) (maximum) is equivalent to:
(if E₁ > E₂ then E₁ else E₂).

3.

(IntAbs) $abs(E) (absolute value) is equivalent to:
(if E < 0 then -E else E).

4.

(OpBin2u) bin2u(E₁, E₂) interprets the E₂ first bits of an array E₁ of bool as an unsigned binary number and is equivalent to:
SUM i : [0, E₂-1] (2 i * (if E₁[i] then 1 else 0)) for a fresh i.

5.

(OpBin2s) bin2s(E₁, E₂) interprets the E₂ first bits of an array E₁ of bool as a signed binary number encoded in the two’s complement notation and is equivalent to:
-(if E₁[E₂-1] then 1 else 0) * 2 (E₂-1) + bin2u(E₁, E₂-1).

6.

(OpU2bin) u2bin(E₁, E₂) converts an integer E₁ into an array of type bool (E₂) and is equivalent to:
(lambda[E₂] : [i] := bit_is_one(E₁, i))
for a fresh i, together with the following declaration and definition (we do not use bitwise and (operator $and) in the definition of bit_is_one since that operator is defined in terms of u2bin):

     Declarations:
      bool bit_is_one(int, int);
     Definitions:
      bit_is_one(E, i) := ((E >> i) - ((E >> (i + 1)) << 1)) == 1;

7.

(OpS2bin) s2bin(E₁, E₂) is equivalent to u2bin(E₁, E₂).

8.

(OpPopCountLt) population_count_lt(E₁, E₂,…E_n,K) of n Boolean streams E_i and an integer stream K is true exactly when less than K of the Boolean streams are true. The expression is reducible to:

((if E₁ then 1 else 0) + (if E₂ then 1 else 0) + ..
.

(if E_n then 1 else 0)) < K

9.

(OpPopCountGt) population_count_gt(E₁, E₂,…E_n, K) is equivalent to ~population_count_lt(E₁, E₂,…E_n, K + 1).

10.

(OpPopCountEq) population_count_eq(E₁, E₂,…E_n, K) is equivalent to ~population_count_lt(E₁, E₂,…E_n, K) &
~population_count_gt(E₁, E₂,…E_n, K)

11.

(OpBitwiseOr) $or(E₁, E₂) (bitwise or) is nil in time step k if either of E₁ or E₂ is nil in time step k. Otherwise the expression is equivalent to bin2s((lambda[C] : [i] := s2bin(E₁, C)[i] # s2bin(E₂, C)[i]), C)
for a fresh i and a constant C. C must be big enough to represent all significant bits of E₁ and E₂, i.e.

\text{[math]}

where ub(E) and lb(E) denote, respectively, the maximum and minimum values the integer expression E may take in any model.

12.

(OpBitwiseXor) $xor(E₁, E₂) (bitwise xor) is equivalent to bin2s((lambda[C] : [i] := s2bin(E₁, C)[i] #! s2bin(E₂, C)[i]), C)
for a fresh i and a constant C. C must be big enough to represent all significant bits of E₁ and E₂, i.e.

\text{[math]}

where ub(E) and lb(E) denote, respectively, the maximum and minimum values the integer expression E may take in any model.

13.

(OpBitwiseNot) $not(E) (bitwise not) is equivalent to bin2s((lambda[C] : [i] := ~s2bin(E, C)[i]), C)
for a fresh i and a constant C. C must be big enough to represent all significant bits of E, i.e.

\text{[math]}

where ub(E) and lb(E) denote, respectively, the maximum and minimum values the integer expression E may take in any model.

14.

(OpBitwiseAnd) $and(E₁, E₂) (bitwise and) is equivalent to $not($or($not(E₁), $not(E₂))).

Static Flag

1.: (FunopUnaryStaticFlag) 𝒮ℱ(∘(E₁)) = 𝒮ℱ(E₁) for ∘∈{$abs, $not}.
2.: (FunopBinaryStaticFlag) 𝒮ℱ(∘(E₁, E₂)) = min(𝒮ℱ(E₁),𝒮ℱ(E₂)) for
∘∈{$min, $max, $and, $xor, $or}.
3.: (FunopNaryStaticFlag) 𝒮ℱ(∘(E₁,…E_n)) = 0 for ∘∈{bin2u, bin2s,
u2bin, s2bin, population_count_lt, population_count_gt,
population_count_eq}.

Restrictions

1.: (FunopUnaryCard) The cardinality of the <expr_list> shall be 1 for the following operators: $abs, $not.
2.: (FunopBinaryCard) The cardinality of the <expr_list> shall be 2 for the following operators:
$min, $max, bin2u, bin2s, u2bin, s2bin, $and, $xor, $or.
3.: (PopCountNumberStatic) 𝒮ℱ(K) ≥ 1 for an expression ∘(E₁,…E_n, K) with
∘∈{population_count_lt, population_count_gt, population_count_eq}.

10.7.7 Cast Expressions

Syntax

(CastExprSyntax)

<cast_expr> ::= "cast" "<" <type> ">" "(" <expr> ")"

Semantics

1.: (CastExpr) A Cast expression cast<T>(E), of type int, is an (unchecked) conversion of an integer expression E into the target type T.
2.: (CastSigned) cast<int signed C>(E) is equivalent to:
bin2s(s2bin(E, C), C).
3.: (CastUnsigned) cast<int unsigned C>(E) is equivalent to:
bin2u(s2bin(E, C), C).
4.: (CastNamedType) cast<T>(E) where T is a named type defined, directly or indirectly, as the type int S (where S is on the form <sign>, see Section 8.1.2) is equivalent to cast<int S>(E).

Static Flag

1.: (CastStaticFlag) 𝒮ℱ(<cast_expr>) = 0.

Restrictions

1.: (CastTargetIntImpl) The target type of a cast shall be an integer implementation type, or a named type that is defined, directly or indirectly, as an integer implementation type.

10.7.8 With Expressions

With expressions can be understood as an operation that creates a modified copy of a composite stream, where a single component has been arbitrarily modified. For example “(A with [0] := ~A[0])” is equivalent to the Boolean array A for all components except the one at index 0, which has been negated. With expressions are particularly useful when translating assignments of an imperative language into HLL.

With expressions can be written with collections on the right hand side (see the definition of <rhs> in Section 12). In order to explain the semantics of with expressions with collections on the right hand side, we expand them into a chain of with expressions, each with a single element of the collection on the right hand side (this expansion would have to be repeated if such an element is in turn another collection). For example: “(A with [0] := {1, 2, 3})” is expanded, assuming the projection expression A[0] is of array type (i.e. A is an array of arrays), into the equivalent formula “(((A with [0][0] := 1) with [0][1] := 2) with [0][2] := 3)”. This expansion is formalised in (WithCollectionRhsUniDim) below.

The multidimensional case, e.g. when A[0] is a multidimensional array (or multivariate function), is a bit trickier and formalised in (WithCollectionRhsMultiDim) below. However, the basic idea is the same.

Syntax

(WithExprSyntax)

<with_expr> ::= "(" <expr> "with" {<accessor>}+ ":=" <rhs> ")"

Forward References

1.: <rhs> is defined in Section 12.

Semantics

1.

(WithCollectionRhsUniDim) (E with A := {R₀,R₁,…R_n−1}) where E A is of type T_{E_A}, which is neither a multidimensional array type nor a multivariate function type, is equivalent to:

(…((E with A A₀ := R₀) with A A₁ := R₁)… with A A_n−1 := R_n−1) where:

( || .i if TEA is tuple {T0,...Tn− 1} { .Mi if TEA is struct {M0 : T0,...Mn−1 : Tn−1} Ai = || [i] if TEA is T^(n) ( (Vi) if TEA is (T1-> T) and T1 is {V0,...Vn−1} with Vi < Vi+1

2.

(WithCollectionRhsMultiDim) (E with A := {R₀,R₁,…R_m₁}) where E A is of type T_{E_A}, which is either a multidimensional array type or a multivariate function type, is equivalent to:

(… (…((E with A A_0…00 := R_0…00) … with A A_{0…0m_k} := R_{0…0m_k})
with A A_0…10 := R_0…10) … with A A_{0…1m_k} := R_{0…1m_k})

                              .
..               .
..                     .
..             .
..

with A A_{0…m_k−10} := R_{0…m_k−10}) … with A A_{0…m_k−1m_k} := R_{0…m_k−1m_k})

with A A_m₁m₂…0 := R_m₁m₂…0) … with A A_{m₁m₂…m_k} := R_{m₁m₂…m_k})

where:

A_{i₁…i_k} =

{ [i1,...ik] if TE is T^(m1 + 1,...mk + 1) = (Vi,...Vi) if TEAis (T1 ∗ ...Tk -> T),T is {V0,...Vm },Vi < Vi+1 1 k A j∈[1,k] j

and R_{i₁…i_k} are constructed inductively:

(base) R_i₁ for i₁ ∈ [0,m₁] are given above (as the elements of the collection).

(step) R_{i₁…i_j} =

( ′ ′ ′ |||| Rij if Ri1...ij−1 is {R0,...Rmj} |||| |||| Ri1...ip[ip+1,...ik] if j = k and Ri1...ip−1 is <collection> and { Ri1...ip is <expr> of type T^(mp+1 + 1,...mk + 1) = || |||| Ri1...ip(Vip+1,...Vik) if j = k and Ri1...ip−1 is <collection> and |||| Ri1...ip is <expr> of type (Tp+1 ∗...Tk-> T) ||( undefined otherwise

3.

(WithMultipleAcc) (E₁ with A₁ A₂…A_n := E₂) is equivalent to (E₁ with A₁ A₂…A_n−1 := (E₁ A₁ A₂…A_n−1 with A_n := E₂)).

4.

(WithArrayAcc) (E₁ with [E₃, E₄,…E_n] := E₂) where E₁ is of type T (C₃, C₄,…C_n) is equivalent to:
(lambda[C₃, C₄,…C_n] : [i₃, i₄,…i_n] :=
if i₃ = E₃ & i₄ = E₄ &…& i_n = E_n then E₂ else E₁[i₃, i₄,…i_n])

where i_j with 3 ≤ j ≤ n are fresh variables.

5.

(WithFunctionAcc) (E₁ with (E₃, E₄,…E_n) := E₂) where E₁ is of type (T₃ ∗T₄ ∗…∗T_n -> T) is equivalent to:
(lambda(T₃, T₄,…T_n) : (i₃, i₄,…i_n) :=
if i₃ = E₃ & i₄ = E₄ &…& i_n = E_n then E₂ else E₁(i₃, i₄,…i_n))

where i_j with 3 ≤ j ≤ n are fresh variables.

6.

(WithTupleStructAcc) (E₁ with .M := E₂) where E₁ is of tuple or struct type T, and E₂ is of type T_M is identical to E₁ for all components except the one designated by M, which is equal to E₂. A formal definition uses the following equation (with an overloading of operator @):

\text{[math]}

Static Flag

1.: (WithExprStaticFlag) 𝒮ℱ(<with_expr>) = 0.

Restrictions

1.: (WithAccCompatible) The accessor A in the expression (E with A := R) must be a compatible accessor w.r.t. the type of E, meaning that the projection expression E A must be a valid expression.
2.: (WithRhsAssignable) The type of the <rhs> R of an expression (E with A := R) shall be assignable to the type of the projection expression E A.

10.7.9 Case Expressions

Syntax

(CaseExprSyntax)

<case_expr>    ::= "(" <expr_list> {<case_item>}+ ")"
<case_item>    ::= "|" <pattern_list> "=>" <expr>
<pattern>      ::= <expr>
                 | <named_type> ( <id> | "_" )
                 | "_"
<pattern_list> ::= <pattern> { "," <pattern> }

Semantics

1.

(CaseExpr) In each time step, a case expression

(E₁, E₂, … E_n |P₁₁, P₁₂, … P_1n => R₁ |P₂₁, P₂₂, … P_2n => R₂ ..
.

|P_m1, P_m2, … P_mn => R_m)

evaluates to the first branch R_i for which all the <pattern> items P_i1 to P_in match the switch expressions E₁ to E_n. Each P_ij is matched against, and only against, the corresponding E_j. The type of the expression is the union of the types of the R_i.

2.

(CasePatternExpr) A <pattern> item E_p which is an <expr> matches a switch expression E_s in time step k iff Mbool(E_p = E_s,k) = true.

3.

(CasePatternType) A <pattern> item T x which is a <named_type> (followed by either an identifier or a wildcard) matches a switch expression E_s in time step k iff Mbool(E_s : T,k) = true.

4.

(CasePatternWildcard) The <pattern> item _ (a wildcard) matches any switch expression E_s (in any time step).

5.

(CaseCapturingVariable) Each <case_item> of a case expression opens a local scope in the namespace of streams, called a Branch scope, that starts at the => and continues to the end of the <case_item>. Given a <pattern> P_ij on the form <named_type> <id> of the <case_item>, the identifier <id> resides in the branch scope, and if the <case_item> is a match in time step k, the <id> refers to a local static stream x of type T (similar to a lambda parameter of Section 10.2), called a Capturing variable, whose value in each time step is equal to MT(E_j,k), i.e. MT(x,n) = M_{T_{E_j}}(E_j,k) for all time steps n. In other words, the capturing variable x refers to a different static stream in each matching time step, and applying a temporal operator such as X or PRE to such a variable has thus no effect.

6.

(CaseExprNil) A case expression propagates nil in a similar manner to an equivalent sequence of if-then-else expressions (see Section 10.1). Furthermore, a case expression evaluates to nil in a time step k if there is no <pattern_list> matching the switch expressions in that time step (the case expression is not exhaustive). In order to formalize this, we will first define the binary function “match”, with signature match : <expr_list>×<pattern_list> → <expr>, as follows:

match({E₁,…E_n},{P₁,…P_n}) =

(| match({E1},{P1}) &...& if n > 1, else |||| match({En},{Pn}) |{ E1 = P1 if P1 is on the form <expr>, else = | E1 : T if P1 is on the form T x where T |||| is a <named type>, else |( true (P1 is on the form "")

Now, given the case expression of (CaseExpr) above, it will evaluate to nil in time step k if one of the following conditions is true:

(a): There is no matching <pattern_list> P_i1,…P_in, i.e. one for which Mbool(match({E₁,…E_n}, {P_i1…P_in}),k) = true, or
(b): There is a <pattern_list> P_j1,…P_jn above the first matching <pattern_list> P_i1,…P_in (i.e. with j < i) such that Mbool(match( {E₁,…E_n}, {P_j1…P_jn}),k) = nil.

(Note that the case expression will of course also evaluate to nil in time step k in case the matching branch R_i evaluates to nil in time step k.)

Static Flag

1.: (CaseExprStaticFlag) 𝒮ℱ(<case_expr>) = 0.
2.: (CaseCapturingVarStaticFlag) 𝒮ℱ(x) = 1 for a capturing variable x corresponding to the <id> of a <pattern> on the form <named_type> <id>.

Restrictions

1.: (CaseSwitchesScalar) The switches in the <expr_list> of a case expression shall be of scalar type.
2.: (CasePatternsCompatible) The number of pattern items (<pattern>) in each <case_item> shall match the number of switches in the <expr_list>, and their types shall be pair-wise compatible, except for wildcards (_).
3.: (CaseBranchesCompatible) The types of the branches (R_i) shall be compatible.
4.: (CasePatternExprConstant) 𝒮ℱ(E) = 2 for a <pattern> E which is an <expr>.
5.: (CasePatternTypeSort) A pattern item <pattern> which is a <named_type> shall refer to a valid sort type.
6.: (CaseCapturingVarUnicity) Two capturing variables of the same branch may not have the same name.

10.7.10 Quantifier Expressions

Quantifiers in HLL usually operate on static domains (sets of values – much like types) to create properties over populations of streams. For example, if we have an array A of 3 integers, declared as int A[3], with the components taking the following values:

The SELECT operator selects the unique value from the domain that satisfies the given predicate. If zero or two (or more) values from the domain satisfy the predicate, then nil is selected instead:

Quantifiers can also be nested, and the domains of nested quantifiers may depend on the quantifier variables of the enclosing ones. So the previous formulation could be optimized to reduce the number of iterations:

Quantification was extended in HLL version 3.0 to allow quantification over (the components of) array and function streams, using the new operator $items. As an example, ALL a:$items(A) (a < 4) is equivalent to ALL i:[0,2] (A[i] < 4) above. As two components of an array or function may be equal, this corresponds to quantification over a domain which is a multiset of streams (of values). To fit easier with the historical quantifiers in the formal definition below, we will use an alternative (but equivalent) point of view and instead define the domain as a stream of multisets (of values). To connect this with our running example, it means that the domain $items(A) corresponds to the following stream of multisets:

The use of multisets instead of sets is important only when considering the SUM and PROD quantifers. For example:

Note that the SELECT operator is not allowed in the combination with a domain on the form $items(A).

²⁰This means that upper bound i of the domain of j in the expression ALL i : [0, 10], j : [0, i] (i >= j) does not refer to the quantifier variable i introduced just before j. On the other hand, in the expression ALL i : [0, 10] ALL j : [0, i] (i >= j), the upper bound of j does refer to the quantifier variable i in the enclosing quantifier expression.

Syntax

(QuantExprSyntax)

<quantif_expr>   ::= <quantifier> <quantif_vars>
                       ( "(" <expr> ")" | <quantif_expr> )
                   | "SELECT" <quantif_vars>
                       ( "(" <expr> ["," <rhs>] ")" |
                         <quantif_expr> )

<quantif_vars>   ::= <quantif_var> {"," <quantif_var>}
<quantif_var>    ::= <id> ":" <quantif_domain>
<quantif_domain> ::= <domain>
                   | "$items" "(" <expr> ")"

<quantifier>     ::= "SOME" | "ALL"  | "SUM"  | "PROD"
                   | "CONJ" | "DISJ" | "$min" | "$max"

Semantics

1.

(QuantScope) A Quantifier expression (<quantif_expr>) introduces a local scope in the namespace of streams, called a Quantifier scope that starts right after the last <quantif_var> and continues to the end of the expression. The quantifier variables (<quantif_var>) exist, and only exist, within this scope.²⁰

2.

(QuantDomainDomain) A quantifier domain D which is a <domain> corresponds for each time step k to the set of values D_k (see Section 10.4). Due to restriction (QuantDomainStatic), such a quantifier domain is guaranteed to be static and not to change from one time step to another.

3.

(QuantDomainItems) A quantifer domain $items(E) where E is of array or function type T_E with component type T corresponds for each time step k to the following multiset of values:

{MT(E A_0…00,k),    MT(E A_0…01,k),   …  MT(E A_{0…0m_n},k),
  MT(E A_0…10,k),    MT(E A_0…11,k),   …  MT(E A_{0…1m_n},k),
                .
..                          .
..            .
..                 .
..
  MT(E A_{0…m_n−10},k),MT(E A_{0…m_n−11},k), …  MT(E A_{0…m_n−1m_n},k),
                ..
.                          ..
.                           ..
.
  MT(E A_m₁m₂…0,k),  MT(E A_m₁m₂…1,k),  …  MT(E A_{m₁m₂…m_n},k) }

where:

A_{i₁…i_n} =

{ [i1,...in] if TE is T^(m1 + 1,...mn + 1) = (Vi ,...Vi ) if TE is (T1 ∗ ...Tn -> T),T is {V0,...Vm } 1 n j∈[1,n] j

4.

(QuantVarType) The type of a quantifer variable i : D is:

(a): The type compatible with D if D is a <domain>, as according to (DomainAsType) and (DomainAsRange).
(b): The component type of the array or function type of E, if D is on the form $items(E).

5.

(QuantMultVar) QTF i₁ : D₁, i₂ : D₂,…i_n : D_n (E), where QTF is a <quantifier> other than SELECT and the i_i : D_i are <quantif_var>, is reducible to QTF j₁ : D₁ (QTF j₂ : D₂ … (QTF j_n : D_n (E<i₁ := j₁,i₂ := j₂, …i_n := j_n>)) …) where j₁ to j_n are fresh identifiers.

6.

(QuantDisj) DISJ is equivalent to SOME.

7.

(QuantConj) CONJ is equivalent to ALL.

8.

(QuantSome) SOME i:D (E), of type bool, evaluates to true in time step k iff there exists some value j in D such that E, with all occurrences of i replaced by j, evaluates to true. Formally:

( { true if ∃j ∈ Dk Mbool (E<i := j>,k) = true Mbool(SOME i : D (E),k) = ( nil if ∃j ∈ Dk Mbool (E<i := j>,k) = nil false otherwise

(Where the cases on the right hand side should be considered in order from top to bottom.)

9.

(QuantAll) ALL i:D (E), of type bool, evaluates to true in time step k iff for all values j in D, E, with all occurrences of i replaced by j, evaluates to true. Formally:

\text{[math]}

(Where the cases on the right hand side should be considered in order from top to bottom.)

10.

(QuantSum) SUM i:D (E), of type int, evaluates to the sum of all E_i. Formally:

Mint(SUM i : D (E),k) =

\text{[math]}

(Where D_k = ∅ means that the domain D is empty at time step k.)

11.

(QuantProd) PROD i:D (E), of type int, evaluates to the product of all E_i. Formally:

Mint(PROD i : D (E),k) =

\text{[math]}

(Where D_k = ∅ means that the domain D is empty at time step k.)

12.

(QuantMin) $min i:D (E), of type int, selects the minimum of all E_i. Formally:

Mint($min i : D (E),k) =

\text{[math]}

(Where D_k = ∅ means that the domain D is empty at time step k.)

13.

(QuantMax) $max i:D (E), of type int, selects the maximum of all E_i. Formally:

Mint($max i : D (E),k) =

\text{[math]}

(Where D_k = ∅ means that the domain D is empty at time step k.)

14.

(QuantSelectDefault) The optional <rhs>, separated by a comma from the <expr>, of a <quantif_expr> with the SELECT operator, denotes the default value, of scalar, tuple or collection type, to select.

15.

(QuantSelectType) The type T_val of the selected value of SELECT i₁ : D₁, i₂ : D₂,…i_n : D_n (E [,R]) is defined as follows:

\text{[math]}

where:

\text{[math]}

The type T of the SELECT expression itself is equal to T_val if there is no default value R. Otherwise, it is defined as the union type (see 8.4.3) of T_val and the type of R

16.

(QuantSelectDomain) The domain D of SELECT i₁ : D₁, i₂ : D₂,…i_n : D_n (E [,R]) is the n-fold Cartesian product D = D₁ ×D₂ ×…×D_n.

Note that the domain of a selection is a static subset of the type T_val defined by (QuantSelectType) above.

17.

(QuantSelectWithoutDefault) At each time step, the selection expression SELECT i₁ : D₁, i₂ : D₂,…i_n : D_n (E) of type T and domain D as given according to (QuantSelectType) and (QuantSelectDomain) respectively, selects the unique value (if n = 1) or tuple value (if n > 1) from the domain D for which the Boolean predicate E is true. To simplify the formal definition below, we will extend the tuple notation to scalar values so that V@0 will mean the same thing as V if the value V is scalar. Formally:

MT(SELECT i₁ : D₁, i₂ : D₂,…i_n : D_n (E),k) =

\text{[math]}

18.

(QuantSelectWithDefault) The selection expression with a default value is similar to the selection without default (see (QuantSelectWithoutDefault)), except in the case where no value in the domain D makes the predicate true at time step k. In that case the default value is selected for time step k. A default value which is a <collection> is then interpreted as a tuple value. Formally:

MT(SELECT i₁ : D₁, i₂ : D₂,…i_n : D_n (E,R),k) =

\text{[math]}

(Where the cases should be considered in order from top to bottom.)

Static Flag

1.: (QuantExprStaticFlag) 𝒮ℱ(<quantif_expr>) = 0.
2.: (QuantVarStaticFlag) The static flag of a quantifier variable i : D (the <id> of a <quantif_var>) is:
$\text{[math]}$

Restrictions

1.: (QuantVarUnicity) Two quantifier variables of a quantifier expression may not have the same name.
2.: (QuantDomainFinite) Quantification is not allowed over an infinite domain.
3.: (QuantDomainNotNil) Quantification is not allowed over a domain taking the value nil in any time step (see (DomainAsRange)).
4.: (QuantDomainStatic) 𝒮ℱ(D) ≥ 1 for a <quantif_var> i : D, where D is a <domain>.
5.: (ItemsOperandArrayOrFunction) The operand E of $items(E) must be either of array type, or of function type (with a finite domain).
6.: (BoolQuantOperandBool) The operand E of QTF V (E) where QTF ∈{SOME,ALL} shall be of type bool.
7.: (IntQuantOperandInt) The operand E of QTF V (E) where QTF ∈{SUM,PROD,$min,$max} shall be of integer type.
8.: (SelectQuantOperandBool) The operand E of SELECT V₁,…V_n (E [,R]) shall be of type bool.
9.: (SelectQuantDefaultCompatible) The operand R of SELECT V₁,…V_n (E [,R]) shall be of a type compatible to the type T_val of the selected value as defined by (QuantSelectType).
10.: (SelectQuantDefaultGround) The operand R of SELECT V₁,…V_n (E,R) shall not make reference to any of the quantifier variables V₁ to V_n. (The following is not allowed: SELECT i:[0,10] (false, i).)
11.: (SelectQuantNoItemsDomain) A quantifier expression with operator SELECT is not allowed in combination with a domain on the form $items(E). In other words, the quantifier variables V_i of SELECT V₁,…V_n (E [,R]) may not be on the form i : $items(E).

11 Declarations

Declarations declare streams with a name and a type. The declared stream is visible everywhere (except where it is hidden) in the scope where the declaration appears, regardless of the position of the declaration within the scope. An example, where all occurrences of x refer to the same variable:

²¹Whether the text is parsed as a <declaration> or as an <input> depends on the context, i.e. whether it occurs in a “declarations section” (<decl_section>) or in an “inputs section” (<inputs_section>) (see Section 16).

Syntax

(DeclarationSyntax)

<declaration>      ::= [<type>] <declarator> {"," <declarator>}
<input>            ::= [<type>] <input_declarator>
                           {"," <input_declarator>}
<input_declarator> ::= <declarator>
                     | "I" "(" <declarator> ")"

Semantics

1.: (Declaration) A Declaration (<declaration> or²¹ <input>) declares a stream with name and type and makes it visible everywhere in its scope (of the namespace of streams), regardless of the position of the declaration.
2.: (DeclMultInline) T D₁, D₂,…D_n is equivalent to the n declarations T D₁, T D₂, …T D_n, regardless of whether the D_i denote <declarator> or <input_declarator>.
3.: (DeclNormal) A <declaration> [T] D declares a (normal) stream variable. The name of the variable corresponds to the first <id> of the declarator D and the Declared Type is calculated according to procedure calc_type in Section 7 using the base type T if given and the declarator D. If no base type T is given, the base type used to calculate the declared type is the type bool.
4.: (DeclInput) An Input declaration (<input>) on the form [T] D (i.e. not an initial input declaration as defined in (DeclInitialInput)) is reducible to a normal declaration (<declaration>) [T] D. (Note the extra restrictions (InputsFinite) and (InputsUndefined) which apply to input declarations.)
5.: (DeclInitialInput) An input declaration (<input>) on the form [T] I(D) is called an Initial input declaration and is reducible to the normal declaration (<declaration>) [T] D. (Note the extra restriction (DeclInitialInputDefNext) which applies to initial input declarations in addition to those for ordinary input declarations.)

Restrictions

1.: (DeclUnicity) A stream variable may not be declared more than once per scope of the namespace of streams.
2.: (InputsFinite) The resulting type (as calculated by calc_type from the base type and the declarator) of an input declaration shall be either scalar or composite with a finite number of components (either directly or indirectly via other composite components).
3.: (InputsUndefined) A stream declared using an input declaration may not be defined, except for initial inputs as specified in (DeclInitialInputDefNext).
4.: (DeclInitialInputDefNext) A stream variable declared using an initial input declaration shall be defined with, and only with, a next definition (see Section 12).
5.: (UndefinedSized) A stream declared (using a normal or an input declaration) but not defined shall be declared using a type that is neither int (without a size restriction), nor a composite type with a component of type int (either directly or indirectly via other composite components).

12 Definitions

Definitions define one or several stream variables on the left hand side of the definition symbol := using an expression or a collection on the right hand side. If the stream variables are undeclared they become implicitly declared by the definition, but only if the type of the right hand side is scalar.

Multiple definitions and circular (non-causal) definitions are not allowed. For example:

If the definition is paired with a declaration, the pair must appear in the same scope. An example:

Syntax

(DefinitionSyntax)

<definition>    ::= <lhs> ":=" <rhs>
                  | "I" "(" <lhs> ")" ":=" <rhs>
                  | "X" "(" <lhs> ")" ":=" <rhs>
                  | <lhs> ":=" <rhs> "," <rhs>
<lhs>           ::= <unfolding>
                  | <id> {<formal_param>}+
<rhs>           ::= <expr>
                  | <collection>
<collection>    ::= "{" <rhs> {"," <rhs>} "}"
<unfold_lhs>    ::= <id> | "_"
<unfolding>     ::= <unfold_lhs> {"," <unfold_lhs>}

Semantics

1.

(Definition) A Definition (<definition>) defines one or several stream variables on the Left hand side (<lhs>) using an expression or collection on the Right hand side (<rhs>).

2.

(DefUndeclared) If a stream variable on the left hand side of a <definition> is undeclared in the scope (excluding ascendant and descendant scopes) of the definition, then it is implicitly declared by the definition and becomes visible everywhere in the scope (of the namespace of streams) of the definition, regardless of the position of the definition. The type of the variable is inferred according to (DefUndeclaredType) below.

3.

(DefUndeclaredType) A stream variable V which is implicitly declared by a definition according to (DefUndeclared) above is assigned the type T according to the following table. T_E denotes the type of the right hand side E.


Definition	Condition	T


X(V) := E	(none)	bool

V := E₁, E₂	(none)	bool

V := E	V is defined (directly or indirectly)	bool
	in terms of itself (recursive definition)

	otherwise	T_E

4.

(DefAlways) V := E (always definition) where E is a stream expression of type T_E and V is a stream variable of type T, defines the value of V in all time steps, using the expression E. Formally, for all time steps k:

{ M (V,k) = MTE(E,k) if MTE(E,k) ∈ T T nil otherwise

5.

(DefInit) I(V) := E (initial definition) defines the value of V of type T, in the first time step only, using the expression E of type T_E. Formally:

{ MT (V,0) = MTE(E,0) if MTE(E,0) ∈ T nil otherwise

6.

(DefNext) X(V) := E (next definition) defines the value of V of type T, in the next time step, using the expression E of type T_E. Formally, for all time steps k:

{ MT (E,k) if MT (E,k) ∈ T MT (V,k+ 1) = nilE otherEwise

7.

(DefLatch) <lhs> := E₁, E₂ (latch definition) is equivalent to the two definitions I(<lhs>) := E₁ and X(<lhs>) := E₂.

8.

(DefFunctionInit) I(V FP):= E is equivalent to the two definitions: I(V):= V′ and V′ FP:= E where V′ is a fresh variable of same type as V.

9.

(DefFunctionNext) X(V FP):= E is equivalent to the two definitions: X(V):= V′ and V′ FP:= E where V′ is a fresh variable of same type as V.

10.

(DefArrayFunction) An Array or Function definition V FP := E is equivalent to V := lambda DS : FP := E where DS is obtained by solving the equation T_V = calc_type(T_E,DS) where T_V is the declared type of V and T_E is the type of E.

11.

(DefCollectionRhs) A <lhs> of ordered composite type may be defined using a collection (<collection>) on the right hand side. In such a case component number k of <lhs> is defined by the <rhs> number k of the collection. Such components may themselves be recursively defined by collections, if they are of ordered composite type. Formally, a definition V := {R₁,…R_n} is equivalent to V := ((lambda[1] : [i] := V′) with [0] := {R₁,…R_n})[0] where V′ is a fresh variable with the same type as V.

The type of a <rhs> which is a <collection> is a collection type as defined in Section 8.4.1.

12.

(DefUnfolding) An Unfolding definition is a definitions where several variables or wildcards ("_") occur comma-separatedly on the left hand side (using an <unfolding>). If the right hand side is of composite type (including collections) with n ordered components then such a definition with k variables and l wildcards, with n = k + l on the left hand side is equivalent to k ordinary definitions (i.e. with a single variable on the left hand side) of the appropriate kind (“always”, “initial” or “next”) where the variable at index i (with 1 ≤ i ≤ n) on the left hand side is defined using the component (or collection element) number i on the right hand side.

Static Flag

1.: (CollectionStaticFlag) 𝒮ℱ(<collection>) = 0.
2.: (DefAlwaysStaticFlag) 𝒮ℱ(V) = min(1,𝒮ℱ(E)) for V := E.
3.: (DefLatchStaticFlag) 𝒮ℱ(V) = 0 for X(V) := E or V := E₁, E₂.

Restrictions

1.: (DefCausality) A scalar stream variable or component may not have its value in time step n be defined, directly or indirectly, in terms of its own value in any time step k ≥ n.
The cyclicity criterion, i.e. the precise criterion for when such a variable or component is considered defined in terms of its own value will depend on the reasoning power of tools implementing HLL – especially when it comes to recursive array and function definitions – and is thus outside the scope of this document.
2.: (DefUnicity) A stream variable may not have its value in time step n be defined more than once.
3.: (DefCompleteness) A stream variable with an initial definition shall also have a next definition. (The converse is not required however, i.e. the initial value may be left undefined/free.)
4.: (DefUndeclaredLhsScalarRhs) If the variable on the <lhs> is undeclared, then there shall be no <formal_param> and the type of the <rhs> shall be scalar.
5.: (DefRhsTypeAssignableToLhsType) The type of the <rhs> shall be assignable to the type of the <lhs>. For this purpose, the type of an <lhs> on the form V FP (where FP corresponds to the {<formal_param>}+) is derived in the same way as for the corresponding projection expression (see Section 10.6).
6.: (LatchesSized) A stream defined with a latch or next definition shall not be declared with a type that is either int (without a size restriction), or a composite type with a component of type int (either directly or indirectly via other composite components).
7.: (DefUnfoldingCompatibleRhs) When the left hand side (<lhs>) of a definition is on the form of an <unfolding>, then the right hand side (<rhs>) shall be of ordered composite type, but shall not be of multidimensional array type nor of multivariate function type, and the number of variables plus the number of wildcards on the left hand side shall equal the number of components of the type of the right hand side.

13 Constants

Syntax

(ConstantSyntax)

<constant> ::= "bool" <id> ":=" <expr>
             | "int" <id> ":=" <expr>

Semantics

1.

(ConstantDef) A Constant definition (<constant>) declares and defines a named constant stream.

2.

(ConstantDefIsaDeclDef) Semantically, T C := E is equivalent to:

     Declarations:
      T C;
     Definitions:
      C := E;

Furthermore, all restrictions that apply to the latter language construct also apply to the former (as according to (ConstantDefInheritedRestrictions)). However, there are two minor differences between the language constructs:

(a): The static flag of C as defined by the former construct is 2 (as according to (ConstantStaticFlag)), whereas it is at most 1 for the C defined by the latter construct (as according to (DefAlwaysStaticFlag) of Section 12).
(b): The additional restriction (ConstantDefRhsConstant) applies only to the former construct.

Static Flag

1.: (ConstantStaticFlag) 𝒮ℱ(C) = 2 for a <constant> T C := E.

Restrictions

1.

(ConstantDefRhsConstant) 𝒮ℱ(E) = 2 for a <constant> T C := E.

2.

(ConstantDefInheritedRestrictions) All restrictions that apply to the language construct:

      Declarations:
       T C;
      Definitions:
       C := E;

also apply to a <constant> T C := E.

14 Constraints

Syntax

(ConstraintSyntax)

<constraint> ::= <expr>
               | "I" "(" <expr> ")"

Semantics

1.: (ConstraintAlways) An Always constraint E (an <expr>) corresponds to the proposition □E.
2.: (ConstraintInitial) An Initial constraint I(E) corresponds to the proposition 𝕀 E.

Restrictions

1.: (ConstraintBool) Constraints shall be expressions of type bool.

15 Proof Obligations

Syntax

Semantics

1.: (PoBool) A Proof obligation (PO) E (an <expr>) of type bool corresponds to the proposition □E.
2.: (PoComposite) A proof obligation E of type T, which is an array or function type with bool as component type, corresponds to the proposition □( ALL e : $items(E) (e) ).
3.: (PoValid) A proof obligation is Valid iff it is a consequence of all the constraints within the same (global) HLL text (regardless of whether the constraints appear in the same user namespace or not). Note that if there is no model M which does not falsify the constraints (for example if the constraints are contradictory), then any proof obligation is trivially valid.
4.: (PoFalsifiable) A proof obligation which is not valid takes the value nil or the value false at some time step k in some model M which does not falsify the constraints. If the proof obligation takes the value nil we say that the proof obligation is not well-defined. Otherwise, if it takes the value false, we say that the proof obligation is Falsifiable.

Restrictions

1.: (PoType) Proof obligations shall be expressions of type bool, or of array or function type with bool as component type. (This means that the types bool^(N) or bool^(N, M) are accepted but not the type bool^(N)^(M).)

16 Sections

Syntax

(SectionSyntax)

<HLL>                ::= {<section>}
<section>            ::= <constants_section>
                       | <types_section>
                       | <inputs_section>
                       | <decl_section>
                       | <def_section>
                       | <outputs_section>
                       | <constr_section>
                       | <po_section>
                       | <namespaces_section>

<constants_section>  ::= <constants> ":"    {<constant> ";"}
<types_section>      ::= <types> ":"        {<type_def> ";"}
<inputs_section>     ::= <inputs> ":"       {<input> ";"}
<decl_section>       ::= <declarations> ":" {<declaration> ";"}
<def_section>        ::= <definitions> ":"  {<definition> ";"}
<outputs_section>    ::= <outputs> ":"      {<expr> ";"}
<constr_section>     ::= <constraints> ":"  {<constraint> ";"}
<po_section>         ::= <proof> <obligations> ":" {<po> ";"}
<namespaces_section> ::= <namespaces> ":"   {<namespace>}

<constants>          ::= "Constants"    | "constants"
<types>              ::= "Types"        | "types"
<inputs>             ::= "Inputs"       | "inputs"
<declarations>       ::= "Declarations" | "declarations"
<definitions>        ::= "Definitions"  | "definitions"
<constraints>        ::= "Constraints"  | "constraints"
<proof>              ::= "Proof"        | "proof"
<obligations>        ::= "Obligations"  | "obligations"
<outputs>            ::= "Outputs"      | "outputs"
<namespaces>         ::= "Namespaces"   | "namespaces"

Semantics

1.: (HLLText) An HLL text (<HLL>) is a (possibly empty) list of sections.
2.: (GlobalTopLevelScopes) The Global top-level scopes of an HLL text <HLL> that is not nested within a <namespace> encompass the entire text.
3.: (SectionOrderIrrelevant) The order of the sections of an HLL text and the order of items within the sections have no impact on the semantics of the text.
4.: (SectionsReopen) Sections may be opened any number of times.

Restrictions

1.: (OutputsFinite) The <expr> in an <outputs> section shall be either of scalar type or of a composite type with a finite number of scalar components (either directly or indirectly via other composite components).

A Syntax Overview

<HLL> ::= {<section>} <section> ::= <constants_section> | <types_section> | <inputs_section> | <decl_section> | <def_section> | <outputs_section> | <constr_section> | <po_section> | <namespaces_section> <constants_section> ::= <constants> ":" {<constant> ";"} <types_section> ::= <types> ":" {<type_def> ";"} <inputs_section> ::= <inputs> ":" {<input> ";"} <decl_section> ::= <declarations> ":" {<declaration> ";"} <def_section> ::= <definitions> ":" {<definition> ";"} <outputs_section> ::= <outputs> ":" {<expr> ";"} <constr_section> ::= <constraints> ":" {<constraint> ";"} <po_section> ::= <proof> <obligations> ":" {<po> ";"} <namespaces_section> ::= <namespaces> ":" {<namespace>} <constants> ::= "Constants" | "constants" <types> ::= "Types" | "types" <inputs> ::= "Inputs" | "inputs" <declarations> ::= "Declarations" | "declarations" <definitions> ::= "Definitions" | "definitions" <constraints> ::= "Constraints" | "constraints" <proof> ::= "Proof" | "proof" <obligations> ::= "Obligations" | "obligations" <outputs> ::= "Outputs" | "outputs" <namespaces> ::= "Namespaces" | "namespaces" <namespace> ::= <id> "{" <HLL> "}" <constant> ::= "bool" <id> ":=" <expr> | "int" <id> ":=" <expr> <type_def> ::= <type> <declarator> {"," <declarator>} | <enum_def> | <sort_def> <declarator> ::= <id> {<declarator_suffix>} <declarator_suffix> ::= "[" <expr_list> "]" | "(" <type_list> ")" <type> ::= "bool" | <integer> | <tuple> | <structure> | <array> | <function> | <named_type> <integer> ::= "int" | "int" <sign> | "int" <range> <sign> ::= "signed" <id_or_int> | "unsigned" <id_or_int> <id_or_int> ::= <id> | <int_literal> <range> ::= "[" <expr> "," <expr> "]" <enum_def> ::= <enumerated> <id> <enumerated> ::= "enum" "{" <id_list> "}" <tuple> ::= "tuple" "{" <type_list> "}" <structure> ::= "struct" "{" <member_list> "}" <sort_def> ::= "sort" [ <sort_contrib> "<" ] <id> <sort_contrib> ::= <path_id_list> | "{" <id_list> "}" <array> ::= <type> "^" "(" <expr_list> ")" <function> ::= "(" <type> {"*" <type>} "->" <type> ")" <named_type> ::= <path_id> <type_list> ::= <type> {"," <type>} <member_list> ::= <id> ":" <type> {"," <id> ":" <type>} <input> ::= [<type>] <input_declarator> {"," <input_declarator>} <input_declarator> ::= <declarator> | "I" "(" <declarator> ")" <declaration> ::= [<type>] <declarator> {"," <declarator>} <po> ::= <expr> <constraint> ::= <expr> | "I" "(" <expr> ")" <definition> ::= <lhs> ":=" <rhs> | "I" "(" <lhs> ")" ":=" <rhs> | "X" "(" <lhs> ")" ":=" <rhs> | <lhs> ":=" <rhs> "," <rhs> <lhs> ::= <unfolding> | <id> {<formal_param>}+ <rhs> ::= <expr> | <collection> <collection> ::= "{" <rhs> {"," <rhs>} "}" <unfold_lhs> ::= <id> | "_" <unfolding> ::= <unfold_lhs> {"," <unfold_lhs>} <formal_param> ::= "[" <id_list> "]" | "(" <id_list> ")" <accessor> ::= "." <id> | "." <int_literal> | "[" <expr_list> "]" | "(" <expr_list> ")" <expr> ::= <ite_expr> | <lambda_expr> | <binop_expr> | <membership_expr> | <unop_expr> | <proj_expr> <ite_expr> ::= "if" <expr> "then" <expr> {"elif" <expr> "then" <expr>} "else" <expr> <lambda_expr> ::= "lambda" {<declarator_suffix>}+ ":" {<formal_param>}+ ":=" <expr> <binop_expr> ::= <expr> <binop> <expr> <membership_expr> ::= <expr> ":" <domain> <domain> ::= <range> | <type_domain> <type_domain> ::= <named_type> | "bool" | "int" <unop_expr> ::= <unop> <expr> <proj_expr> ::= <closed_expr> { <accessor> } <closed_expr> ::= <bool_literal> | <int_literal> | <named_expr> | <next_expr> | <pre_expr> | <fun_expr> | <cast_expr> | <with_expr> | <case_expr> | <quantif_expr> | "(" <expr> ")" <bool_literal> ::= <true> | <false> <dec_literal> ::= [0-9](_?[0-9])* <bin_literal> ::= 0[Bb][0-1][_?[0-1])* <hex_literal> ::= 0[Xx][0-9A-Fa-f](_?[0-9A-Fa-f])* <int_literal> ::= <dec_literal> | <hex_literal> | <bin_literal> <named_expr> ::= <path_id> <next_expr> ::= "X" "(" <expr> ")" <pre_expr> ::= ("pre" | "PRE") ["<" <type> ">"] "(" <expr> ["," <expr>] ")" <fun_expr> ::= <fop> "(" <expr_list> ")" <cast_expr> ::= "cast" "<" <type> ">" "(" <expr> ")" <with_expr> ::= "(" <expr> "with" {<accessor>}+ ":=" <rhs> ")" <case_expr> ::= "(" <expr_list> {<case_item>}+ ")" <case_item> ::= "|" <pattern_list> "=>" <expr> <pattern> ::= <expr> | <named_type> ( <id> | "_" ) | "_" <pattern_list> ::= <pattern> { "," <pattern> } <quantif_expr> ::= <quantifier> <quantif_vars> ( "(" <expr> ")" | <quantif_expr> ) | "SELECT" <quantif_vars> ( "(" <expr> ["," <rhs>] ")" | <quantif_expr> ) <quantif_vars> ::= <quantif_var> {"," <quantif_var>} <quantif_var> ::= <id> ":" <quantif_domain> <quantif_domain> ::= <domain> | "$items" "(" <expr> ")" <binop> ::= "#" | "&" | "#!" | "->" | "<->" | ">" | ">=" | "<" | "<=" | "=" | "==" | "!=" | "<>" | "+" | "-" | "*" | "%" | "^" | "<<" | ">>" | "/" | "/>" | "/<" <unop> ::= "~" | "-" <fop> ::= "$min" | "$max" | "$abs" | "$or" | "$and" | "$xor" | "$not" | "bin2u" | "u2bin" | "bin2s" | "s2bin" | "population_count_eq" | "population_count_lt" | "population_count_gt" <expr_list> ::= <expr> {"," <expr>} <id_list> ::= <id> {"," <id>} <path_id_list> ::= <path_id> {"," <path_id>} <path_id> ::= <relative_path> <id> | <absolute_path> <id> <relative_path> ::= { <id> "::" } <absolute_path> ::= "::" { <id> "::" } <id> ::= regexp: [a-zA-Z_][a-zA-Z0-9_]* | regexp: ’[^\n’]+’ | regexp: "[^\n"]+" <true> ::= "true" | "TRUE" | "True" <false> ::= "false" | "FALSE" | "False" <quantifier> ::= "SOME" | "ALL" | "SUM" | "PROD" | "CONJ" | "DISJ" | "$min" | "$max"

A.1 Operator Precedence and Associativity

The precedence of expressions is given below in order from lowest to highest (same line means same precedence). The information below is a copy of (ExprPrecedence).

The precedence of the binary operators is given below in order from lowest to highest, together with their associativity. Same line means same precedence. The information below is a copy of (BinopGrouping).

B Reserved Words

C Restrictions Overview

Below are listed the direct and indirect restrictions which apply to each language construct of HLL. The indirect restrictions, as explained in Section 2.4.2, are due to language constructs being defined by translation or reduction to other language constructs which in turn have restrictions on them. These restrictions also apply, indirectly, to the language constructs defined by the translation or reduction, and are thus listed in the table below.

On the other hand, some language constructs contain sub-constructs which have specific restrictions applied to them. The restrictions which apply to sub-constructs are not listed as applicable to the parent construct (to avoid duplication). An example is projections, <proj_expr>, which are defined using the sub-construct <accessor> where specific restrictions apply.

When a restriction applies only to a certain part of a language construct, we will occasionally, for the benefit of the reader and especially if the restriction is indirect, prefix the restriction with the part of the language construct to which it applies.

D Glossary

For the purposes of this document, the following terms and abbreviations are used.

1.

ascendant scope
an enclosing scope, i.e. one higher up in the scope stack; see Section 2.3

2.

ASCII
American Standard Code for Information Interchange, a character encoding standard

3.

assignable / assignability
refers to the assignability relation between types, see Section 8; a stream expression E₁ is assignable to a stream expression E₂ iff the type of E₁ is assignable to the type of E₂

4.

combinatorial function
a mapping from values to values (usually a mapping from one or several values to a single value)

5.

combinatorial operator
see combinatorial function

6.

compatible / compatibility
(sometimes preceded by type) refers to the compatibility relation between types, see Section 8; a stream expression E₁ is compatible with a stream expression E₂ iff the type of E₁ is compatible with the type of E₂

7.

component
either a component (type) of a composite type, or a component (stream) of a stream of composite type; similar terms used elsewhere would be e.g. struct field, array element, function output – all those entities are collectively called components in this document

8.

composite
equivalent to non-scalar;
(noun) a stream of composite type
(adj.) applied to a stream it means a composite stream; applied to a type it means a composite type; applied to a value it means a value of a composite type

9.

composite type
equivalent to non-scalar type; any type defined in Section 8.2

10.

consequence
see Section 2.1.4

11.

constant
refers either to a stream defined using the nonterminal <constant> of Section 13, or to any stream with a static flag of 2.

12.

declared type
see Section 11

13.

defined variable
a variable with a definition, i.e. that occurs on the left hand side of a definition; see Section 12

14.

descendant scope
an enclosed scope, i.e. one further down in the scope stack; see Section 2.3

15.

directly defined
(adj.) refers to an entity E₁ which is defined in terms of another entity E₂ without there being any intermediate entity E₃ in between E₁ and E₂; see also indirectly defined

16.

domain
depending on the context, refers to one of:

(a): the nonterminal <domain>, defined in Section 10.4,
(b): the nonterminal <quantif_domain>, defined in Section 10.7.10,
(c): the parameter types of a function type, see Section 8.2.3,
(d): the domain of an array type, which amounts to the parameter types of the equivalent function type, see Section 8.2.4, or
(e): the domain of the SELECT operator, which is defined by (QuantSelectDomain).

17.

EBNF
Extended Backus-Naur Form, see also Section 2.4.1

18.

equivalent to
see Section 2.4.2

19.

explicit grouping
the process of adding parentheses around all subexpressions (or groups) in a text; for example, expressions such as “a & b & c” and “a + b * c” are explictly grouped into respectively “((a & b) & c)” and “(a + (b * c))”

20.

free
(adj.) applied to a variable it means a variable that is free to take any value of its type in each time step; input variables are free; quantifier variables or defined variables are not free

21.

fresh
(adj). applied to the identifier of an entity it means that another entity with the same identifier is not visible within the same namespace; (an entity with a fresh name does not hide another entity)

22.

function accessor
see (AccFunction) of Section 9

23.

function value
see combinatorial function

24.

group / grouping
see implicit grouping or explicit grouping

25.

hide / hiding
refers to variable hiding see Section 2.3

26.

HLL
High Level Language

27.

HLL function
a stream of combinatorial functions (function values) which, together with a function accessor, maps streams to streams by point-wise application of the combinatorial function in each time step on the values of the stream operands in the same time step; HLL functions are distinct from temporal functions which are general mappings of streams to streams

28.

iff
if and only if

29.

implicit grouping
the process by which a parser uses syntax, precedence and associativity rules to map a text into an abstract syntax tree (AST) where each group (or subexpression) is represented by its own vertex

30.

implicit input
(sometimes followed by variable) a free variable that is not an (explicit) input

31.

indirectly defined
(adj.) refers to an entity E₁ which is defined in terms of another entity E₂ via an intermediate entity E₃; e.g. E₁ := E₃; E₃ := E₂;

32.

initial input
(sometimes followed by variable) a memory variable which is undefined in the first time step (i.e. it has only a next definition, see Section 12)

33.

input
(sometimed preceded by explicit; sometimes followed by variable) refers to variables declared using the nonterminal <input>, see Section 11

34.

integer implementation type
see Related Notation 1 of Section 8.1.2

35.

integer range type
see Related Notation 2 of Section 8.1.2

36.

integer type
any type defined in Section 8.1.2

37.

latch
(sometimes followed by variable) a variable defined using a latch or a next definition, see Section 12

38.

literal
(sometimes followed by value) refers to an immediate value such as the integer literal 1234 or the Boolean literal true.

39.

memory
either a pre expression or a latch; if followed by variable it means a latch.

40.

model
(sometimes preceded by stream) see Section 2.1.1.

41.

multidimensional
(adj). applied to an array type it means that the type has more than one dimension, see Section 8.2.4

42.

multivariate
(adj). applied to a function type it means that the type has more than one parameter type, see Section 8.2.3

43.

namespace
see Section 2.3; not to be confused with user namespace

44.

nil
see Section 2.1.2

45.

parameter
refers to the nonterminal <formal_param> defined in Section 10.2

46.

proposition
see Section 2.1.3

47.

qualified
(adj). applied to a path identifier (<path_id>) it means a path identifier with at least one occurrence of "::". See Section 5.1

48.

reducible to
see Section 2.4.2

49.

scalar
(noun) a stream of scalar type
(adj.) applied to a stream it means a scalar stream; applied to a type it means a scalar type; applied to a value it means a value of a scalar type

50.

scalar type
any type defined in Section 8.1

51.

scope
see Section 2.3

52.

significant bit
a significant bit of an integer encoded in two’s complement is a bit which cannot be removed from the encoding without changing the encoded value; leading 0s and 1s are not significant, meaning that the numbers 000 and 0 both encode 0, 001 and 01 both encode +1, and 111 and 1 both encode −1

53.

static flag
see Section 2.1.5

54.

stream
a stream of values of a certain type, see Section 10

55.

temporal function
a mapping from streams to streams

56.

temporal operator
see temporal function

57.

type
a tool for the classification of streams which can be understood simply as a set of values, see Section 8

58.

undefined variable
see free variable

59.

unsized copy
see Section 8.4.2

60.

user namespace
see Section 5; not to be confused with namespace

61.

value
a mathematical object that is the element or member of a type, for example the Boolean value “true”, the integer value “1234”, or the enum value “blue”; composite values (i.e. values of composite types) can be represented by n-tuples where n corresponds to the number of components of the composite type, for example “(true,1234)”; if a value V is used in a context where a stream is expected, it is interpreted as a constant stream that takes the value V in each time step

62.

variable
(often preceded by stream) a stream variable, i.e. a named stream (that can be referenced if it is visible)

63.

visible / visibility
refers to variable visibility, see Section 2.3

Label Index

AccArray, 53
AccFunction, 53
AccStruct, 53
AccTuple, 53
AccessorSyntax, 53
ArrayAssignability, 47
ArrayCompatibility, 47
ArrayDimConstant, 47
ArrayDimNotNil, 47
ArrayIndexInteger, 53
ArraySyntax, 47
ArrayType, 47
ArrayValues, 47
BinopGrouping, 60
BinopStaticFlag, 60
BinopSyntax, 60
BoolAnd, 60
BoolAssignability, 35
BoolCompatibility, 35
BoolEquiv, 60
BoolImpl, 60
BoolLitFalse, 67
BoolLitStaticFlag, 67
BoolLitSyntax, 67
BoolLitTrue, 67
BoolNeg, 63
BoolNegOperandBool, 63
BoolOr, 60
BoolOrEquivOperandsBool, 60
BoolQuantOperandBool, 82
BoolSyntax, 35
BoolValueOrder, 35
BoolValues, 35
BoolXor, 60
CaseBranchesCompatible, 79
CaseCapturingVarStaticFlag, 79
CaseCapturingVarUnicity, 79
CaseCapturingVariable, 79
CaseExpr, 79
CaseExprNil, 79
CaseExprStaticFlag, 79
CaseExprSyntax, 79
CasePatternExpr, 79
CasePatternExprConstant, 79
CasePatternType, 79
CasePatternTypeSort, 79
CasePatternWildcard, 79
CasePatternsCompatible, 79
CaseSwitchesScalar, 79
CastExpr, 74
CastExprSyntax, 74
CastNamedType, 74
CastSigned, 74
CastStaticFlag, 74
CastTargetIntImpl, 74
CastUnsigned, 74
ClosedExprSyntax, 66
CollArrayAssignability, 50
CollFuncAssignability, 50
CollMultiDimArrayAssignability, 50
CollMultiVarFuncAssignability, 50
CollTupleCompatibility, 50
CollTupleStructAssignability, 50
CollectionReason, 50
CollectionStaticFlag, 88
CollectionType, 50
CommentDoubleSlash, 23
CommentSlashStar, 23
ConstantDef, 89
ConstantDefInheritedRestrictions, 89
ConstantDefIsaDeclDef, 89
ConstantDefRhsConstant, 89
ConstantStaticFlag, 89
ConstantSyntax, 89
ConstraintAlways, 90
ConstraintBool, 90
ConstraintInitial, 90
ConstraintSyntax, 90
DeclArrayDimConstant, 32
DeclArrayDimInteger, 32
DeclFunctionParamScalar, 32
DeclInitialInput, 85
DeclInitialInputDefNext, 85
DeclInput, 85
DeclMultInline, 85
DeclNormal, 85
DeclUnicity, 85
Declaration, 85
DeclarationSyntax, 85
Declarator, 32
DeclaratorSyntax, 32
DeclaratorTypeCalc, 32
DefAlways, 88
DefAlwaysStaticFlag, 88
DefArrayFunction, 88
DefCausality, 88
DefCollectionRhs, 88
DefCompleteness, 88
DefFunctionInit, 88
DefFunctionNext, 88
DefInit, 88
DefLatch, 88
DefLatchStaticFlag, 88
DefNext, 88
DefRhsTypeAssignableToLhsType, 88
DefUndeclared, 88
DefUndeclaredLhsScalarRhs, 88
DefUndeclaredType, 88
DefUnfolding, 88
DefUnfoldingCompatibleRhs, 88
DefUnicity, 88
Definition, 88
DefinitionSyntax, 88
Domain, 62
DomainAsRange, 62
DomainAsType, 62
DomainScalar, 62
Elif, 55
EmptyScalarTypeNil, 54
EnumAssignability, 38
EnumCompatibility, 38
EnumDef, 38
EnumSyntax, 38
EnumValueDef, 38
EnumValueOrder, 38
EnumValueSpace, 38
EnumValueStaticFlag, 38
EnumValueUnicity, 38
EqOperandsFiniteCompatible, 60
Expr, 54
ExprPrecedence, 54
ExprSyntax, 54
FormalParamStaticFlag, 58
FunctionAssignability, 46
FunctionCompOrder, 46
FunctionCompatibility, 46
FunctionDomainEquality, 46
FunctionDomainScalar, 46
FunctionInputScalar, 53
FunctionSyntax, 46
FunctionType, 46
FunctionValues, 46
FunopBinaryCard, 73
FunopBinaryStaticFlag, 73
FunopNaryStaticFlag, 73
FunopSyntax, 73
FunopUnaryCard, 73
FunopUnaryStaticFlag, 73
GlobalTopLevelScopes, 93
GroupedExpr, 66
GroupedExprStaticFlag, 66
HLLText, 93
Id, 25
IdOrInt, 37
IdSignificantChars, 25
IdSyntax, 25
IfThenElse, 55
InlineMultTypeDef, 34
InputsFinite, 85
InputsUndefined, 85
IntAbs, 73
IntAdd, 60
IntAssignability, 37
IntCeilDiv, 60
IntCompatibility, 37
IntCoreBinopOperandsInt, 60
IntDiv, 60
IntExp, 60
IntFloorDiv, 60
IntGt, 60
IntGte, 60
IntLeftShift, 60
IntLitBinary, 68
IntLitDecimal, 68
IntLitHexadecimal, 68
IntLitStaticFlag, 68
IntLitSyntax, 68
IntLitUnderscores, 68
IntLiteral, 68
IntLt, 60
IntLte, 60
IntMax, 73
IntMin, 73
IntMul, 60
IntNeg, 63
IntNegOperandInt, 63
IntQuantOperandInt, 82
IntRangeValues, 37
IntRem, 60
IntRightShift, 60
IntSignedValues, 37
IntSizeConstant, 37
IntSizeInteger, 37
IntSizeNotNil, 37
IntSub, 60
IntSyntax, 37
IntUnsignedValues, 37
IntValueOrder, 37
IntValues, 37
IteBranchesCompatible, 55
IteCondBool, 55
IteExprStaticFlag, 55
IteExprSyntax, 55
ItemsOperandArrayOrFunction, 82
LambdaArray, 58
LambdaDeclSuffixOverhang, 58
LambdaExprSyntax, 58
LambdaFunction, 58
LambdaMultFormalParam, 58
LambdaParamUnicity, 58
LambdaParamsBound, 58
LambdaParamsMatch, 58
LambdaScope, 58
LambdaStaticFlag, 58
LambdaType, 58
LambdaTypeCheck, 58
LatchesSized, 88
Membership, 62
MembershipDomainCompatible, 62
MembershipPrecedence, 62
MembershipStaticFlag, 62
MembershipSyntax, 62
NamedExpr, 69
NamedExprImplicitDecl, 69
NamedExprStaticFlag, 69
NamedExprSyntax, 69
NamedExprUndefinedStaticFlag, 69
NamedType, 48
NamedTypeAssignability, 48
NamedTypeCompatibility, 48
NamedTypeRef, 48
NamedTypeSyntax, 48
NamespaceSyntax, 26
NextExpr, 70
NextExprStaticFlag, 70
NextExprSyntax, 70
OpBin2s, 73
OpBin2u, 73
OpBitwiseAnd, 73
OpBitwiseNot, 73
OpBitwiseOr, 73
OpBitwiseXor, 73
OpEqCompositeMultiDim, 60
OpEqCompositeUniDim, 60
OpEqEq, 60
OpEqScalar, 60
OpNeq, 60
OpPopCountEq, 73
OpPopCountGt, 73
OpPopCountLt, 73
OpS2bin, 73
OpU2bin, 73
OutputsFinite, 93
PathAbsolute, 28
PathId, 28
PathIdLookup, 28
PathIdNoImplicitDecl, 28
PathIdSyntax, 28
PathRelative, 28
PoBool, 91
PoComposite, 91
PoFalsifiable, 91
PoSyntax, 91
PoType, 91
PoValid, 91
PopCountNumberStatic, 73
Pragma, 24
PreExprStaticFlag, 71
PreExprSyntax, 71
PreOperandsAssignable, 71
PreTyped, 71
PreTypedWithInit, 71
PreUntyped, 71
PreUntypedWithInit, 71
PreUppercase, 71
ProjAccCompatible, 65
ProjArrayFunc, 65
ProjExprNil, 65
ProjExprStaticFlag, 65
ProjExprSyntax, 65
ProjMultipleAcc, 65
Projection, 65
QuantAll, 82
QuantConj, 82
QuantDisj, 82
QuantDomainDomain, 82
QuantDomainFinite, 82
QuantDomainItems, 82
QuantDomainNotNil, 82
QuantDomainStatic, 82
QuantExprStaticFlag, 82
QuantExprSyntax, 82
QuantMax, 82
QuantMin, 82
QuantMultVar, 82
QuantProd, 82
QuantScope, 82
QuantSelectDefault, 82
QuantSelectDomain, 82
QuantSelectType, 82
QuantSelectWithDefault, 82
QuantSelectWithoutDefault, 82
QuantSome, 82
QuantSum, 82
QuantVarStaticFlag, 82
QuantVarType, 82
QuantVarUnicity, 82
RangeDomainStaticFlag, 62
ReservedWords, 25
SecondShiftOperandNonNegative, 60
SecondShiftOperandStatic, 60
SectionOrderIrrelevant, 93
SectionSyntax, 93
SectionsReopen, 93
SelectQuantDefaultCompatible, 82
SelectQuantDefaultGround, 82
SelectQuantNoItemsDomain, 82
SelectQuantOperandBool, 82
SignedBitsPositive, 37
SortAssignability, 40
SortCompatibility, 40
SortContrib, 40
SortContribScope, 40
SortDef, 40
SortSubTypeContrib, 40
SortSubTypes, 40
SortSyntax, 40
SortUnionAssignability, 52
SortUnionCompatibility, 52
SortValueContrib, 40
SortValueOrder, 40
SortValueSpace, 40
SortValueStaticFlag, 40
SortValueUnicity, 40
StructAssignability, 43
StructCompIdSpace, 43
StructCompUnicity, 43
StructCompatibility, 43
StructSyntax, 43
StructType, 43
StructValues, 43
TupleAssignability, 42
TupleCompatibility, 42
TupleSyntax, 42
TupleType, 42
TupleValues, 42
Type, 34
TypeAssignability, 34
TypeCalc, 34
TypeCompatibility, 34
TypeDef, 34
TypeDefCausality, 34
TypeDefUnicity, 34
TypeDomainStaticFlag, 62
TypeIdSpace, 34
TypeSyntax, 34
UndefinedSized, 85
UnionComposite, 52
UnionScalar, 52
UnionSort, 52
UnionTupleCollection, 52
UnopStaticFlag, 63
UnopSyntax, 63
UnsignedBitsNonNegative, 37
UnsizedComposite, 51
UnsizedInteger, 51
UnsizedScalar, 51
UserNamespace, 26
UserNamespaceName, 26
UserNamespaceScattering, 26
WithAccCompatible, 77
WithArrayAcc, 77
WithCollectionRhsMultiDim, 77
WithCollectionRhsUniDim, 77
WithExprStaticFlag, 77
WithExprSyntax, 77
WithFunctionAcc, 77
WithMultipleAcc, 77
WithRhsAssignable, 77
WithTupleStructAcc, 77

E How to Contact Prover Technology

If you have questions or comments concerning this document, or want to report an error or omission, you are welcome to contact our support staff at:

We welcome your comments on our products, so please do not hesitate to contact us.

Proposition	Meaning
𝕀 s	s is true in time step 0
□s	s is always true

Static Flag	Informal Meaning
𝒮ℱ(s) = 0	s is not known to be static
𝒮ℱ(s) = 1	s is static
𝒮ℱ(s) = 2	s is static and a combination of only constants and literal values

Relation	Type	Meaning
C₁ is equivalent to C₂	equivalence relation	Either of C₁ and C₂ can be used in place
	(reflexive, symmetric	of the other, without change of meaning
	transitive)	or correctness, anywhere in an HLL text
		in which all subexpressions have been
		explicitly grouped⁵.

C₁ is reducible to C₂	preorder	C₂ can be used in place of C₁, without
	(reflexive, transitive)	change of meaning or correctness,
		anywhere in an HLL text in which all
		subexpressions have been explicitly
		grouped.

Character		ASCII value
’\0’	(null character)	0

Characters		ASCII values
’\t’	(horizontal tab)	9
’\n’	(new line)	10
’\r\n’	(carriage return followed by new line)	13, 10
’ ’	(white space)	32

Language Construct	Parent Construct	Applicable Restrictions
Section 4
<id>		(ReservedWords)
Section 5
<path_id>		(PathIdNoImplicitDecl)
Section 7
<declarator_suffix>		(DeclArrayDimInteger)
		(DeclArrayDimConstant)
		(DeclFunctionParamScalar)
Section 8
<type> <declarator>	<type_def>	(TypeDefUnicity)
		(TypeDefCausality)
<enum_def>	<type_def>	(TypeDefUnicity)
		(TypeDefCausality)
<sort_def>	<type_def>	(TypeDefCausality)
int signed E	<integer>	(IntSizeInteger)
		(IntSizeConstant)
		(SignedBitsPositive)
		(IntSizeNotNil)
int unsigned E	<integer>	(IntSizeInteger)
		(IntSizeConstant)
		(UnsignedBitsNonNegative)
		(IntSizeNotNil)
int [E₁,E₂]	<integer>	(IntSizeInteger)
		(IntSizeConstant)
		(IntSizeNotNil)
<enumerated>	<enum_def>	(EnumValueUnicity)
{V₁,V₂,…V_n}	<sort_contrib>	(SortValueUnicity)
sort S₁,S₂,…S_k < S	<sort_def>	(SortSubTypes)
<member_list>	<structure>	(StructCompUnicity)
<function>		(FunctionDomainScalar)
<array>		(ArrayDimConstant)
		(ArrayDimNotNil)
<named_type>		(NamedTypeRef)
Section 9
[E₁, E₂,…E_n]	<accessor>	(ArrayIndexInteger)
(E₁, E₂,…E_n)	<accessor>	(FunctionInputScalar)

HLLLanguage Definition

Legal Notice

History

Author

Authors of previous versions

Revision History

Contents

1 Introduction

1.1 Purpose

1.2 Definitions, Terms and Abbreviations

1.3 Overview

2 Preliminaries

2.1 Streams

2.1.1 Models

2.1.2 Exceptional Value

2.1.3 Propositions

2.1.4 Consequences

2.1.5 Static Flag

2.2 Logic of Exceptions

2.3 Namespaces and Scoping

2.4 Notation

2.4.1 Syntax-Related Notation

2.4.2 Semantics-Related Notation

2.5 Document Structure

2.5.1 Language Construct Example

3 Lexical Structure

3.1 Comments

3.2 Pragmas

4 Identifiers

5 User Namespaces

5.1 Path Identifiers

6 Lists

7 Declarators

8 Types

8.1 Scalar Types

8.1.1 Boolean Type

8.1.2 Integer Types

8.1.3 Enum Types

8.1.4 Sort Types

8.2 Composite Types

8.2.1 Tuple Types

8.2.2 Struct Types

8.2.3 Function Types

8.2.4 Array Types

8.3 Named Types

8.4 Implicit Types

8.4.1 Collection Types

8.4.2 Unsized Types

8.4.3 Union Types

9 Accessors

10 Expressions

10.1 If-Then-Else Expressions

10.2 Lambda Expressions

10.3 Binop Expressions

10.4 Membership Expressions

10.5 Unop Expressions

10.6 Projection Expressions

10.7 Closed Expressions

10.7.1 Boolean Literals

10.7.2 Integer Literals

10.7.3 Named Expressions

10.7.4 Next Expressions

10.7.5 Pre Expressions

10.7.6 Function-Style Expressions

10.7.7 Cast Expressions

10.7.8 With Expressions

10.7.9 Case Expressions

10.7.10 Quantifier Expressions

11 Declarations

12 Definitions

13 Constants

14 Constraints

15 Proof Obligations

16 Sections

A Syntax Overview

A.1 Operator Precedence and Associativity

B Reserved Words

C Restrictions Overview

D Glossary

Label Index

HLL
Language Definition