FO[Int]¶

The goal of FO[Int] is to allow expressing knowledge about integer quantities using the 4 arithmetic operators and comparisons. It extends FO[PF].

It also allows creating and using types containing a range of elements, and the comparison of dates, e.g., to determine the applicability of a law..

Integer arithmetic¶

Lexicon

Token

Pattern

Example

COMPARISON

=<|≤|<|~=|≠|=|>|≥|>=

INT

Int|ℤ

INTEGER

[+-]?\d+

-123

MULT_DIV

⨯|\*|\/|%

POWER

\^

SUM_MINUS

+|-

UNARY

-|~|¬

Note that this extension extends the pattern of UNARY in FO[Core].

Syntax

    Type ← INT;

Conjunction  ← Comparison  {AND           Comparison};
Comparison   ← { ANNOT }
SumMinus    {COMPARISON    SumMinus};
SumMinus     ← MultDiv     {SUM_MINUS     MultDiv};
MultDiv      ← Power       {MULT_DIV      Power};
Power        ← Unary       {POWER         Unary};

Identifier ← INTEGER;
Symbol ← 'abs';


Note that this extension replaces the syntax of a Conjunction in FO[Core].

flowchart LR subgraph Conjunction direction LR start{ } --> Comparison([Comparison]); Comparison --> END{ }; Comparison --> AND; AND --> Comparison2([Comparison]); Comparison2 --> AND; Comparison2 --> END; end;
flowchart LR subgraph Comparison direction LR start{ } --> SumMinus([SumMinus]); SumMinus --> END{ }; SumMinus --> COMPARISON; COMPARISON --> SumMinus2([SumMinus]); SumMinus2 --> COMPARISON; SumMinus2 --> END; end;
flowchart LR subgraph SumMinus direction LR start{ } --> MultDiv([MultDiv]); MultDiv --> END{ }; MultDiv --> SUM_MINUS; SUM_MINUS --> MultDiv2([MultDiv]); MultDiv2 --> SUM_MINUS; MultDiv2 --> END; end;
flowchart LR subgraph MultDiv direction LR start{ } --> Power([Power]); Power --> END{ }; Power --> MULT_DIV; MULT_DIV --> Power2([Power]); Power2 --> MULT_DIV; Power2 --> END; end;
flowchart LR subgraph Power direction LR start{ } --> Unary([Unary]); Unary --> END{ }; Unary --> POWER; POWER --> Unary2([Unary]); Unary2 --> POWER; Unary2 --> END; end;

Well-formedness

1. Division must be well-guarded to prevent division by 0 (e.g., if y ≠ 0 then x/y else 1).

2. Quantification over ℤ is not allowed (relaxed in FO[Infinite]).

Semantics

The arithmetic and comparison operators have their usual meaning.

Range¶

Syntax

    TypeInterpretation ← '{' INTEGER '..' INTEGER '}';
Quantee ← VARIABLE {',' VARIABLE} IN '{' INTEGER '..' INTEGER '}';
Enum    ← Base IN '{' INTEGER '..' INTEGER '}';
Identifier ← INTEGER;


Well-formedness

The first INTEGER must be below the second INTEGER.

If the interpretation of a range is not given in the vocabulary block (but in the theory or structure block), it is required to state that the declared type is a subtype of Int.

Semantics

{1..8} represents the set {1, 2, 3, 4, 5, 6, 7, 8}. The type that it interprets is automatically inferred to be a subtype of Int.

Date¶

Lexicon

Token

Pattern

Example

DATE

#\d{4}-\d{2}-\d{2}

#2022-01-01

Syntax

    Type ← 'Date';
Identifier ← DATE | '#TODAY' ['(' INTEGER, INTEGER, INTEGER ')'];


Well-formedness

1. Dates can occur wherever integers can occur.

2. DATE must be a valid date.

3. Quantification over Date is not allowed (except with the FO[Infinite] extension).

Semantics

Dates are converted to proleptic Gregorian ordinals, where January 1 of year 1 has ordinal 1.

#TODAY(y,m,d) is today’s date shifted by y years, m month and d days. #TODAY(-1, 0, 0) is today last year.