Questions tagged [operational-semantics]
Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms.
4
questions
5
votes
1answer
855 views
What does ⊢ mean in operational semantics?
I have been reading a couple of texts on operational semantics.
In [1], the evaluation of expressions is done as in this rule:
$\frac{<e_1,s>\;\Rightarrow \;n_1\;\;\;<e_2,s>\;\Rightarrow ...
33
votes
1answer
10k views
Difference Between Small and Big-step Operational Semantics
What's the fundamental difference(s) between small and big-step operational semantics?
I'm having a hard time grasping what it is and the motivation for having the two.
18
votes
2answers
3k views
What is this fraction-like “discrete mathematics”–style notation used for formal rules?
In the paper "A Conflict-Free Replicated JSON Datatype", I encountered this notation for formally defining "rules":
What is this notation called? How do I read it?
For example:
the ...
3
votes
1answer
74 views
What is the significance of ⟨B, s⟩ -> ⟨B', s'⟩ as the initial rule in this question about small-step semantics?
Revising for an exam and I'm trying to get to grips with operational semantics. Here's the exam question that prompted me posting this:
Exam Question:
We add to the language $\mathsf{SIMP}$ two new ...
