Week 4 Flashcards
What is denotational semantics?
a method used to formally define the meaning of programming constructs by mapping them to mathematical objects
focuses on what a program means rather than how it is executed, providing a precise understanding of its behavior using mathematical structures like sets and functions
What is partial correctness?
addresses whether a program, when it terminates, reaches the correct state according to a specified specification
verifies if the program produces the desired output when it halts, assuming it does indeed terminate
“partial” because it doesn’t consider whether the program will always terminate (which is covered by total correctness), but only concerns itself with correctness upon termination
Three principles of the Classical View of Programs?
- Denotational semantics
- Partial correctness
- Nontermination is bad
What is a reactive system?
a system that responds to stimuli from its environment
focuses on communication and interaction
often parallel
nontermination is good
e.g., operating systems, mobile phones, vending machines
What are the two views on reactive systems?
- A process performs an action and becomes another process (Labelled Transition Systems)
- A process changes state and becomes another process (Kripke Structure)
What is a Kripke Structure? Formal definition
A tuple (S, s0, ->, AP, L) where:
S is a set of states
s0 is the initial state
-> (subset of S * S) is a total transition relation
AP is a set of atomic propositions
L:S -> 2^(AP) is a labelling function that assigns a set of atomic propositions to every state
What is a Kripke Structure? Informal definition
A graph representing the behaviour of the system, where:
The nodes (circles) represent reachable states.
The edges (arrows) represent transitions between state.
The labelling function maps aech state to a set of properties that hold in that state.
What is a path “pi” in a Kripke structure?
A path pi starting in state s is a sequence of states pi = s,s1,s2,s3,s4,… such that s->s1 and si-1 -> si for all i>0
“pi”[i] represents the state at position i in the path pi
“pi”[i…] represents the suffix of the path pi starting at position i
What is PROMELA?
A programming language that can be used to model Kripke structures
Main Components of a PROMELA Model
- Type declarations
- Channel declarations
- Variable declarations
- Process declarations
- “init” process
Data Types in PROMELA
- Five Basic types:
- bit (0/1)
- bool (false/true)
- byte (0, 255)
- short(many more integers)
- int (even more integers) - Arrays:
- e.g., byte a[27] or bit flags[4] - Records:
- e.g.,:
typedef Rectangle {
int width;
int height;
}
Rectangle rr;
rr.width = …
- Message Types/ Enumerations:
- e.g.,:
mtype:fruit = {apple, pear};
mtype:size = {small, medium};
Defining a process body in PROMELA
e.g.,:
proctype Name(int parameter) {
x = 1; //assignment
skip; // no action
int y = 1; // assignment
x < 2 && y == 1; // code waits here until this is satisfied
}
Executability of Statements in PROMELA:
A statement is either executable or it is blocked.
if the process arrives at a blocked statement, it will stop
statements like skip, assignments, declarations, printf are always executable
an expression is executable if it evaluates to true (or a non zero value)
Non-deterministic choice in PROMELA
if statements where multiple if branches are true
if none are true, if-statement blocks
e.g.,
if
:: (true) -> skip;
:: (false) -> skip:
:: else -> skip;
fi
Loops in PROMELA
Use do-statements
very similar to if-statement as it needs conditions and any of the true branches may be taken
however once this is finished, the loop returns to the beginning
break statements can be used to transfer control to the end of the do-statement
do
:: (true) -> skip;
:: (false) -> skip;
else -> skip;
od
How can one instantiate a process in PROMELA?
Processes can be instantiated by using the run keyword.
E.g., for process bruh, run(bruh) instantiates this process
