Skip to content

State the assumptions on Symbols, MaxOffset and BuffSz #230

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
lemmy wants to merge 1 commit into
base: master
Choose a base branch
from
Open

State the assumptions on Symbols, MaxOffset and BuffSz #230

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 18 additions & 1 deletion specifications/braf/BufferedRandomAccessFile.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,10 @@ EXTENDS Naturals, Sequences, TLC, Common

CONSTANT BuffSz

\* Seek's `pos \div BuffSz` needs a nonzero divisor, and Inv2 is unsatisfiable
\* when BuffSz = 0.
ASSUME BuffSzIsPositive == BuffSz \in Nat \ {0}

VARIABLES
\* in-memory variables (BufferedRandomAccessFile class fields)
dirty,
Expand Down Expand Up @@ -380,13 +384,26 @@ Spec == Init /\ [][Next]_vars
\* This module contains constants and definitions common to both
\* RandomAccessFile and BufferedRandomAccessFile.

EXTENDS Naturals, Sequences
EXTENDS Naturals, Sequences, FiniteSets

CONSTANTS
Symbols, \* data stored in the file (in reality there are 256 symbols: bytes 0x00 to 0xFF)
ArbitrarySymbol, \* special token for an arbitrary symbol (to reduce the need for nondeterministic choice)
MaxOffset \* the highest possible offset (in reality this is 2^63 - 1)

\* DiskF and TruncateOrExtendFile mention ArbitrarySymbol explicitly, so
\* Permutations(Symbols) is an unsound SYMMETRY set unless it is not a symbol.
ASSUME ArbitrarySymbolIsDistinct == ArbitrarySymbol \notin Symbols

\* Permutations requires a finite set, as does enumerating SymbolOrArbitrary.
ASSUME SymbolsIsFinite == IsFiniteSet(Symbols)

\* Not needed for soundness; without it every offset holds ArbitrarySymbol.
ASSUME SymbolsIsNonEmpty == Symbols # {}

\* Offset == 0..MaxOffset types curr, lo, diskPos, length, and file_pointer.
ASSUME MaxOffsetIsNat == MaxOffset \in Nat

\* The set of legal offsets
Offset == 0..MaxOffset

Expand Down
Loading