SSL OpenFlow_Action.thy

Sprache: Isabelle

theory OpenFlow_Action
imports
OpenFlow_Matches
begin

(* Beware the differences between Actions and Instructions. OF1.0 doesn't support the former and they're thus not modelled here. *)

(* OF1.0 says actions are a list and executed in-order, OF1.5 has two things: an action set with fixed order in 5.6 and an action list.
So\<dots> list. *)

(* Just those which we need(ed). *)
datatype of_action = Forward (oiface_sel: string) | ModifyField_l2dst "48 word"
(* Note that the 1.0 is not entirely clear that there's no drop action. 1.5 clarifies that this is represented by and empty instruction/action set. *)

(* So each flow entry has a list of these. Semantics\<dots> The actions are executed in order, but the order of the side-effects is not defined. *)
fun of_action_semantics where
"of_action_semantics p [] = {}" |
"of_action_semantics p (a#as) = (case a of
Forward i ==> insert (i,p) (of_action_semantics p as) |
ModifyField_l2dst a ==> of_action_semantics (p(p_l2dst := a)) as)"

value "of_action_semantics p []" (* Drop *)
value "of_action_semantics p [ModifyField_l2dst 66, Forward ''oif'']" (* set mac and send *)

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet am 2026-06-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.