Understanding States, Behaviors, and State Machines in Programming
In programming, states represent assignments of values to variables, and executions are sequences of states. State machines capture these executions, while behaviors are specific subsets of executions. This content delves into the concept of state machines, behaviors, and their significance in software development.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
States, Behaviors, and State Machines 1
So far weve been manipulating mathematical primitives (booleans, integers, predicates, functions) Now we re going to use them to build a structure we ll use repeatedly: state machines and behaviors A state is an assignment of values to variables. An execution is a sequence of states. We re going to capture executions with state machines. 2
The Switch state machine chapter03/demo01.dfy Activate, Toggle Activate off on Deactivate Deactivate, Toggle Activate Activate Toggle Toggle off on on off on 3
Game of Nim chapter03/demo02.dfy Play(1) Play(3) Play(2) Play(4) 11 10 7 5 1 4
Play(1) Play(3) Play(2) Play(4) 11 10 7 5 1 11 10 9 8 7 !Init() 0 11 10 11 8 7 !Next() 5
a state is an assignment of values to variables datatype Card = Shelf | Patron(name: string) datatype Book = Book(title: string) type Library = map<Book, Card> The state space is the set of possible assignments. The Martian: Jon Snow Crash: Jon The Martian: Shelf Snow Crash: Shelf The Martian: Shelf Snow Crash: Jon The Martian: Manos Snow Crash: Jon 6
an execution is an infinite sequence of states check out check out check in check out The Martian: Shelf Snow Crash: Shelf The Martian: Shelf Snow Crash: Jon The Martian: Manos Snow Crash: Jon The Martian: Shelf Snow Crash: Jon The Martian: Rob Snow Crash: Jon check out check in check out check in The Martian: Shelf Snow Crash: Shelf The Martian: Jon Snow Crash: Shelf The Martian: Shelf Snow Crash: Shelf The Martian: Rob Snow Crash: Shelf The Martian: Shelf Snow Crash: Shelf check out check out The Martian: Shelf Snow Crash: Shelf The Martian: Shelf Snow Crash: Jon The Martian: Shelf Snow Crash: Rob 7
a behavior is a subset of executions that we care about check out check out *terminology differs from Lamport check in check out The Martian: Shelf Snow Crash: Shelf The Martian: Shelf Snow Crash: Jon The Martian: Manos Snow Crash: Jon The Martian: Shelf Snow Crash: Jon The Martian: Rob Snow Crash: Jon check out check in check out check in The Martian: Shelf Snow Crash: Shelf The Martian: Jon Snow Crash: Shelf The Martian: Shelf Snow Crash: Shelf The Martian: Rob Snow Crash: Shelf The Martian: Shelf Snow Crash: Shelf check out check out The Martian: Shelf Snow Crash: Shelf The Martian: Shelf Snow Crash: Jon The Martian: Shelf Snow Crash: Rob 8
how should we define a behavior? with a program? its variables define its state space its executions define its behaviors Weaknesses: concreteness nondeterminism asynchrony environment 9
how should we define a behavior? with a state machine its type defines its state space its initial states and transitions define its behaviors 10
datatype Card = Shelf | Patron(name: string) datatype Book = Book(title: string) type Library = map<Book, Card> a state machine definition predicate Init(v: Library) { book | book s :: s[book] == Shelf } predicate CheckOut(v, v , book, patron) { s[book] == Shelf ( book | book v :: v[book] != Patron(patron)) v == v[book := Patron(patron)] } predicate CheckIn(v, v , book, patron) { v[book] == Patron(patron) v == v[book := Shelf] } predicate Next(v, v ) { ( book, patron :: CheckOut(v, v , book, patron)) ( book, patron :: CheckIn(v, v , book, patron)) } enabling condition update Nondeterministic definition 11
a specification is a subset of behaviors that we care about check out check out check in check out predicate CheckOut(v, v , book, patron) { s[book] == Shelf The Martian: Shelf Snow Crash: Shelf The Martian: Shelf Snow Crash: Jon book | book v :: v[book] != Patron(patron) v == v[book := Patron(patron)] } predicate CheckIn(v, v , book, patron) { v[book] == Patron(patron) v == v[book := Shelf] } The Martian: Manos Snow Crash: Jon The Martian: Shelf Snow Crash: Jon The Martian: Rob Snow Crash: Jon check out check in check out check in The Martian: Shelf Snow Crash: Shelf The Martian: Jon Snow Crash: Shelf The Martian: Shelf Snow Crash: Shelf The Martian: Rob Snow Crash: Shelf The Martian: Shelf Snow Crash: Shelf check out The Martian: Shelf Snow Crash: Shelf The Martian: Shelf Snow Crash: Jon The Martian: Shelf Snow Crash: Rob 12
State machine limitations Note that neither programs nor state machines can define every possible behavior (think uncomputable functions). But they re plenty powerful for our practical goals of modeling - - - - programs adversarial components of the environment distributed systems desired application behavior 13
State machine strengths Abstraction States can be abstract: model an infinite map instead of an efficient pivot table Next predicate is nondeterministic: implementation may only select some of the choices can model freedom of Murphy (crash tolerance) or an adversary (integrity) 14
State machine strengths Abstraction Asynchrony Each step of a state machine is conceptually atomic Interleaved steps capture asynchrony: threads, host processes, adversaries Designer decides how precisely to model interleaving; can refine/reduce 15
State machine strengths Abstraction Asynchrony Environment model a proposed program with one state machine (verified) model adversarial environment with another (trusted) compound state machine models their interactions (trusted) System (environment assumption) Filesystem (program to verify) Disk (environment assumption) 16
Lets prove a safety invariant! predicate Safety(v:Library) { forall name :: HasAtMostOneBook(v, name) } Base case predicate Inv(v: Library) { Safety(v) } Inductive Step lemma SafetyProof() ensures forall v :: Init(v) ==> Inv(v) ensures forall v, v' :: Inv(v) && Next(v, v') ==> Inv(v') ensures forall v :: Inv(v) ==> Safety(v) { } Thrilling conclusion 17
Lets prove a safety invariant! predicate Safety(v:Library) { forall name :: HasAtMostOneBook(v, name) } predicate Inv(v: Library) { Safety(v) } lemma SafetyProof() ensures forall v :: Init(v) ==> Inv(v) ensures forall v, v' :: Inv(v) && Next(v, v') ==> Inv(v') ensures forall v :: Inv(v) ==> Safety(v) { } 18
Lets prove a safety invariant! chapter03/demo03.dfy Interactive proof development in editor bisection debugging, case analysis, skolemization 19
Jay Normal Form chapter03/demo04.dfy As you begin writing more interesting specs proofs will be nontrivial. Pull all the nondeterminism into one place, and get a receipt. image: flickr/afagen CC-by-nc-sa 20
Chapter 3 exercise preview You're building specs. Check in office hours to see if your spec made sense! Asking about prior chapters in office hours is always okay. 21
