libtlafmt 0.4.1

A formatter library for TLA+ specs, core of tlafmt
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/ProtoReals.tla
---
------------------------------ MODULE ProtoReals -------------------------------
EXTENDS Peano

IsModelOfReals(R, Plus, Times, Leq) ==
    LET IsAbelianGroup(G, Id, _+_ ) ==
        /\ Id \in G
        /\ \A a, b \in G: a + b \in G
        /\ \A a \in G: Id + a = a
        /\ \A a, b, c \in G: (a + b) + c = a + (b + c)
        /\ \A a \in G: \E minusa \in G: a + minusa = Id
        /\ \A a, b \in G: a + b = b + a
        (**********************************************************************)
     (* Plus and Times are functions and Leq is a set, but it's more       *)
     (* convenient to turn them into the infix operators +, *, and \leq    *)
     (**********************************************************************)
        a + b == Plus[a, b]
        a * b == Times[a, b]
        a <= b == << a, b >> \in Leq
    IN
        /\ Nat \subseteq R
        /\ \A n \in Nat: Succ[n] = n + Succ[Zero]
        /\ IsAbelianGroup(R, Zero, +)
        /\ IsAbelianGroup(R \ {Zero}, Succ[Zero], *)
        /\ \A a, b, c \in R: a * (b + c) = (a * b) + (a * c)
        /\ \A a, b \in R:
            /\ (a <= b) \/ (b <= a)
            /\ (a <= b) /\ (b <= a) <=> (a = b)
        /\ \A a, b, c \in R:
            /\ (a <= b) /\ (b <= c) => (a <= c)
            /\ (a <= b) =>
                /\ (a + c) <= (b + c)
                /\ (Zero <= c) => (a * c) <= (b * c)
        /\ \A S \in SUBSET R:
                LET SBound(a) == \A s \in S: s <= a
                IN (\E a \in R: SBound(a)) =>
                    (\E sup \in R:
                        /\ SBound(sup)
                        /\ \A a \in R: SBound(a) => (sup <= a))

THEOREM \E R, Plus, Times, Leq : IsModelOfReals(R, Plus, Times, Leq)
--------------------------------------------------------------------------------
RM == CHOOSE RM: IsModelOfReals(RM.R, RM.Plus, RM.Times, RM.Leq)

Real == RM.R
--------------------------------------------------------------------------------
Infinity == CHOOSE x: x \notin Real
MinusInfinity == CHOOSE x: x \notin Real \union {Infinity}

a + b == RM.Plus[a, b]

a * b == RM.Times[a, b]

a <= b == CASE (a \in Real) /\ (b \in Real) -> << a, b >> \in RM.Leq
    [] (a = Infinity) /\ (b \in Real \union {MinusInfinity}) -> FALSE
    [] (a \in Real \union {MinusInfinity}) /\ (b = Infinity) -> TRUE
    [] (a = b) -> TRUE

a - b == CASE (a \in Real) /\ (b \in Real) -> CHOOSE c \in Real: c + b = a
    [] (a \in Real) /\ (b = Infinity) -> MinusInfinity
    [] (a \in Real) /\ (b = MinusInfinity) -> Infinity

a / b == CHOOSE c \in Real: a = b * c

Int == Nat \union {Zero - n: n \in Nat}
--------------------------------------------------------------------------------
a ^ b ==
    LET RPos == {r \in Real \ {Zero}: Zero <= r}
        exp == CHOOSE f \in [(RPos \X Real) \union (Real \X RPos)
            \union ((Real \ {Zero}) \X Int) -> Real]:
            /\ \A r \in Real:
                /\ f[r, Succ[Zero]] = r
                /\ \A m, n \in Int: (r /= Zero) =>
                    (f[r, m + n] = f[r, m] * f[r, n])
            /\ \A r \in RPos:
                    /\ f[Zero, r] = Zero
                    /\ \A s, t \in Real: f[r, s * t] = f[f[r, s], t]
                    /\ \A s, t \in RPos: (s <= t) => (f[r, s] <= f[r, t])
    IN exp[a, b]
================================================================================