Questions tagged [small-step-semantics]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
1
vote
0answers
49 views

Small step vs big step semantics for static analysis?

To be an honest question poster I do not yet fully grasp the difference between small step and big step semantics. There was a good discussion here My question is if I were to do static analysis on ...
0
votes
0answers
30 views

Object-oriented small-step semantics NOT based on rewriting techniques

I am looking for a formalized (imperative and possibly statement based) small-step semantics of a subset of an object oriented programming language that it is not based on rewriting techniques. (e.g., ...
2
votes
1answer
82 views

How does one prove that Big Step semantics and Small Step semantics are equivalent for IMP?

I know there is this paper but I wanted to do a special case proof for just IMP for fun. So the theorem is: $$ \langle P , \sigma \rangle \to_{Big} \langle \{ \} , \sigma' \rangle \iff \exists N \...
3
votes
1answer
64 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 ...
1
vote
1answer
59 views

How to express taking the next bit of an infinite string in small-step semantics?

I have to write a rule as part of a small step operational semantics (https://en.wikipedia.org/wiki/Operational_semantics). Whenever this rule is applied, the next bit belonging to an infinite bit ...
26
votes
1answer
6k 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.
2
votes
1answer
690 views

Small-step semantics: for-loops

I'm trying to construct the small-step semantic rules involving the for-loops, but I can't find anything about it in the literature (only about while-loops). I was wondering if anyone could help me ...
4
votes
2answers
217 views

TAPL: Explanation and example(s) for satisfied

This question arises from my reading of "Types and Programming Languages" (WorldCat) by Benjamin C. Pierce. On page 36 is the definition for satisfied A rule is satisfied by a relation if, for ...
4
votes
2answers
282 views

How does one deduce small step operational semantics?

This question arises from my reading of "Types and Programming Languages" (WoldCat) by Benjamin C. Pierce. For the small step operational semantic evaluation rules for the arithmetic expressions (NB) ...