Source code for lyra.semantics.backward

"""
Backward Semantics
==================

Lyra's internal backward semantics of statements.

:Authors: Caterina Urban
"""


from lyra.semantics.semantics import Semantics, DefaultSemantics

from lyra.abstract_domains.state import State
from lyra.core.statements import Assignment, Call


[docs]class BackwardSemantics(Semantics): """Backward semantics of statements.""" pass
[docs]class UserDefinedCallSemantics(BackwardSemantics): """Backward semantics of user-defined function/method calls.""" # noinspection PyUnusedLocal
[docs] def user_defined_call_semantics(self, stmt: Call, state: State): """Backward semantics of a user-defined function/method call. :param stmt: call statement to be executed :param state: state before executing the call statement :return: state modified by the call statement """ error = f"Backward semantics for call statement {stmt} not yet implemented!" raise NotImplementedError(error)
[docs]class AssignmentSemantics(BackwardSemantics): """Backward semantics of assignments."""
[docs] def assignment_semantics(self, stmt: Assignment, state: State) -> State: """Backward semantics of an assignment. :param stmt: assignment statement to be executed :param state: state before executing the assignment :return: state modified by the assignment """ lhs = self.semantics(stmt.left, state).result # lhs evaluation rhs = self.semantics(stmt.right, state).result # rhs evaluation return state.substitute(lhs, rhs)
# noinspection PyAbstractClass
[docs]class DefaultBackwardSemantics(DefaultSemantics, UserDefinedCallSemantics, AssignmentSemantics): """Default backward semantics of statements.""" pass