Linear Temporal Logic:
https://www.cs.colostate.edu/~france/CS614/Slides/Ch5-Summar...(for Xφ, I prefer to define it as relative to a given frame: φ holds the next time any of the frame variables change, which allows both continuous<->discrete translation and for Lamport's stuttering [to allow abstraction!])
Next up: GC via creation and annihilation operators? (in my algebraic view of informatics, one is often either structuring by cleaving two parts to make a whole, or destructuring by cleaving a whole into two parts)
EDIT: and by past-oriented I mean using "was ever" for "eventually" and in the past for "globally", as well as "since" for "until". rotate t by i^2. Eg
dirty := F{edit} U ({save} ∨ {load})
says the local buffer differs from the cloud if there was ever an edit since a save or load.
EDIT 2: ...and I'm pretty sure I can autogenerate code that turns these kinds of def'ns into an imperative event-driven state machine; one can of course come up in theory with formulae that require an arbitrarily complex implementation, but I think in practice most def'ns (especially if we provide backpressure by signalling the complexity of the resulting imp) would be satisfied with simple ones.
(for Xφ, I prefer to define it as relative to a given frame: φ holds the next time any of the frame variables change, which allows both continuous<->discrete translation and for Lamport's stuttering [to allow abstraction!])
Next up: GC via creation and annihilation operators? (in my algebraic view of informatics, one is often either structuring by cleaving two parts to make a whole, or destructuring by cleaving a whole into two parts)
EDIT: and by past-oriented I mean using "was ever" for "eventually" and in the past for "globally", as well as "since" for "until". rotate t by i^2. Eg
says the local buffer differs from the cloud if there was ever an edit since a save or load.EDIT 2: ...and I'm pretty sure I can autogenerate code that turns these kinds of def'ns into an imperative event-driven state machine; one can of course come up in theory with formulae that require an arbitrarily complex implementation, but I think in practice most def'ns (especially if we provide backpressure by signalling the complexity of the resulting imp) would be satisfied with simple ones.