Documentation

Input Data Description

In: The input section defines the program’s data declarations, specifying variable names and their associated sets or types. These declarations follow specific syntax and naming rules:

Elementary Sets and Declaration Syntax

• Format: variable_name ∈ Set
• Variable names start with a lowercase letter
• Set/type names (e.g., N, Z, R, L, S, C, K) start with uppercase
• Multiple declarations separated by commas
• Common elementary sets:
  • N: natural numbers
  • Z: integers
  • R: real numbers
  • L: logical (Boolean) values
  • S: strings/texts
  • C: character set
• Example: a ∈ N , b ∈ Z , name ∈ S

Intervals

• Defined with square brackets and two dots: [start..end]
• Both ends inclusive, represent ranges of values for variables
• Examples: [1..3] , [0..] for open-ended intervals

Indexed Sequences and Arrays

• Collections of elements of the same type indexed over a range
• Syntax: x ∈ N[1..n] means x is an array of natural numbers indexed from 1 to n
• Arrays considered members of the set of all such sequences over the specified index domain
• Index referencing with brackets: x[i]
• Index ranges can be positive, negative, or open-ended (e.g., -1..1 , 1..)
• Functions to query array length and bounds:
  • length(x): length of the array
  • start(x): start” index
  • end(x): end index
• Arrays may be initialized with values, e.g., x6 ∈ N[] = [^5][^1][^2]
• Index bounds can be expressions, e.g., x7 ∈ N[2+3..n*2]

Matrices

• Two-dimensional arrays indexed by two ranges
• Syntax: m ∈ Z[rows, columns] e.g., m1 ∈ Z[1..8, 1..8]
• Access elements with m[row, col] or nested indexing m[row][col] (both understood contextually)
• Open-ended or zero-based indexing possible, e.g., m3 ∈ Z[0.., 0..]
• Initial values can be specified with nested lists, e.g.,

m5 ∈ Z[-1..1,-1..1] = [
  [2, 1, 2],
  [1, 0, 1],
  [2, 1, 1]
]

Records (Structures, Objects)

• Compound data aggregating values of different types into named fields
• Represented as direct product sets of field name and set pairs
• Record names start with a uppercase letter
• Example:

R=(a:S x b:N)

• Arrays of records are accessed like this: `words∈R[1..n]
• Fields accessed by dot notation, e.g., r1.name , r1.grade
• Parentheses allow grouping record types, e.g. (name: S x grade: N)
• Complex records can include multiple logical fields or records as tuples

Unique Set Names (Type Aliases)

• Sets and types can be aliased with new uppercase names for clarity
• Syntax: NewSetName = ExistingSet
• Aliasing can form chains, e.g.:

Mark = FromOneToFive
FromOneToFive = [1..5]

• Used for clearer descriptions of complex or repetitive data types
• Examples:

Student = (name: S x grade: N)
StudentArray = Student2[]
Student2 = (name: S x grades: Grade[])

Scripting Language Syntax Rules for Declarations

• Use lowercase initial letter for variables
• Use uppercase initial letter for sets/types
• Multiple declarations separated by commas ( ,)
• Membership indicated by either ∈ or eleme
• Indexed arrays and matrices use bracket notation for indices
• Initial values assigned with = , using list [ ] or nested lists for arrays/matrices

Auxiliary Data Description

Auxiliary data are intermediary variables used during computation or output preparation.

• Declared like input variables, in the Aux: section
• Must be included in the submitted data
• Follows the same syntax as inputs, e.g., sa ∈ N

Output Data Description

Out:

• Output variables declared similarly to inputs
• Example: ki ∈ L , y ∈ N[]

Function Definitions

Functions are defined similarly to their mathematical form:

• Syntax template:

Fn: function_name : domain -> codomain,
function_definition

• Domain and codomain are sets
• Body supports arithmetic expressions, tuple constructions
• Examples:
  • Doubling: Fn: f: N -> N, f(p) = p * 2
  • Sum of two integers: Fn: add: Z x Z -> Z, add(a,b) = a + b
  • Swap tuple: Fn: swap: Z x Z -> Z x Z, swap(a,b) = (b,a)
  • Function accessing outer variable: Fn: f2 : Z -> Z, f2(p) = p + n
  • Field access function: Fn: grade: Student -> N, grade(h) = h.grade
  • Array element function: Fn: index: N[] x N -> N, index(x,i) = x[i]

Preconditions for Input Data

Preconditions are logical formulas that must hold for the input for the program to be validly executed.

• Logical operators:
  • and
  • or
  • not
• Comparison operators: = , < , > , <= , >=
• Quantifiers supported:
  • ∀ (For all)
  • ∃ (There exists)
• Complex nested expressions with parentheses allowed
• Examples:

Pre: true and not false and 3=3 and n>0 and ...

(simplest always true precondition)

• Array and interval quantifications:
  • ∀i ∈ [1..3]: i > 0
  • ∃i ∈ [1..n]: x[i] < 3
• Matrix quantifiers support nested row and column quantifications
• Records and tuples fields can be accessed by name/index in logic

Postconditions

• Postconditions specify output requirements depending on input
• Must mention all declared variables (input and output)
• Use the same logical notation as preconditions
• Example trivial postcondition: Post: true
• Frequently use quantifiers for expressing existential or universal conditions

Pre built functions

• f(i) is a value-producing function evaluated at index i (e.g., array element, or some expression computed from arrays/records at i).
• A(i) is a boolean condition (predicate) evaluated at index i that decides whether i “qualifies” (true/false

1. Summation (SUM)

Explanation: Calculates the sum of values of a function (or array elements) over an index interval.

In:   b ∈ Z, e ∈ Z
Out:  s ∈ H
Pre:  b ≤ e
Post: s = SUM(i = b..e, f(i))

2. Counting (COUNT)

Explanation: Counts how many indices in an interval satisfy a given condition.

In:   b ∈ Z, e ∈ Z
Out:  cnt ∈ N
Pre:  b ≤ e
Post: cnt = COUNT(i = b..e, A(i))

3. Maximum Selection (MAX)

Explanation: Finds the index and value of the maximum element of a function/array over an interval.

In:   b ∈ Z, e ∈ Z
Out:  maxind ∈ Z, maxval ∈ H
Pre:  b ≤ e
Post: (maxind, maxval) = MAX(i = b..e, f(i))

4. Minimum Selection (MIN)

Explanation: Like MAX, but for the minimum element.

In:   b ∈ Z, e ∈ Z
Out:  minind ∈ Z, minval ∈ H
Pre:  b ≤ e
Post: (minind, minval) = MIN(i = b..e, f(i))

5. Copy (COPY)

Explanation: Creates a sequence by mapping a function over an interval.

In:   b ∈ Z, e ∈ Z
Out:  y ∈ H[1..e-b+1]
Pre:  b ≤ e
Post: y = COPY(i = b..e, f(i))

6. Multiple Item Selection (MIS)

Explanation: Collects the values $f(i)$ for which condition $A(i)$ holds, and returns the count too.

In:   b ∈ Z, e ∈ Z
Out:  cnt ∈ N, y ∈ H[1..cnt]
Pre:  b ≤ e
Post: (cnt, y) = MIS(i = b..e, A(i), f(i))

7. Search (SEARCH)

Explanation: Finds the first index in an interval where a condition holds; returns an existence flag and the index.

In:   b ∈ Z, e ∈ Z
Out:  exists ∈ L, ind ∈ Z
Pre:  b ≤ e
Post: (exists, ind) = SEARCH(i = b..e, A(i))

8. Decision (EXISTS)

Explanation: Decides whether there exists an index in the interval where a condition holds.

In:   b ∈ Z, e ∈ Z
Out:  exists ∈ L
Pre:  b ≤ e
Post: exists = EXISTS(i = b..e, A(i))

9. Decision all (FORALL)

Explanation: Decides whether a condition holds for all indices in the interval.

In:   b ∈ Z, e ∈ Z
Out:  all ∈ L
Pre:  b ≤ e
Post: all = FORALL(i = b..e, A(i))

10. Conditional Maximum (CONDMAX)

Explanation: Finds maximum value (and its index) among those elements that satisfy an additional condition.

In:   b ∈ Z, e ∈ Z
Out:  exists ∈ L, maxind ∈ Z, maxval ∈ H
Pre:  b ≤ e
Post: (exists, maxind, maxval) = CONDMAX(i = b..e, f(i), A(i))

11. Conditional Minimum (CONDMIN)

Explanation: Like CONDMAX, but selects the minimum under the condition.

In:   b ∈ Z, e ∈ Z
Out:  exists ∈ L, minind ∈ Z, minval ∈ H
Pre:  b ≤ e
Post: (exists, minind, minval) = CONDMIN(i = b..e, f(i), A(i))

12. Select (SELECT)

Explanation: Returns the leftmost index $\ge b$ where the condition becomes true, assuming such an index exists.

In:   b ∈ Z, e ∈ Z
Out:  ind ∈ Z
Pre:  ∃ i ∈ [b..e] : A(i)
Post: ind = SELECT(i ≥ b, A(i))

Usage and Evaluation

• Write full specification with sections: Input, Auxiliary, Output, Pre, Post, Functions
• Specification editor supports Ctrl+Space for base structure generation
• Input data can be provided in JSON or YAML format matching declared structures
• “Evaluate” button runs stepwise validation and program simulation (good for debugging)

Example Specification and Usage

Task

Ratbert counted how many times each keyword appears in a code. List the keywords whose counts are greater than the largest count of any keyword that comes before them in the list.

1’st example input: number of keywords: 5 keywords.

Specification

In: n∈N, words∈Te[1..n],Te=(a:S x b:N)
Out: outp∈S[1..]
Fn: attr: N->L,
    attr(i)=(MAX(j=1..i-1,words[j].b).maxval<words[i].b)
Pre: -
Post: (,outp)=MIS(i=1..n,attr(i),words[i].a)

Example Input Data (YAML):

 n: 5
 words:
   - a: program
     b: 1
   - a: if
     b: 10
   - a: else
     b: 5
   - a: while
     b: 20
   - a: ado
     b: 12
 outp:
   - "if"
   - "while"

Reduction table