pub trait SpecCombinator {
type Type;
// Required methods
spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)>;
spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8>;
// Provided methods
open spec fn wf(&self, v: Self::Type) -> bool { ... }
fn requires(&self) -> bool { ... }
}Expand description
Specification for parser and serializer Combinators. All Vest combinators must implement this
trait.
Required Associated Types§
Required Methods§
Sourcespec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)>
spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)>
The specification of Combinator::parse.
Sourcespec fn spec_serialize(&self, v: Self::Type) -> Seq<u8>
spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8>
The specification of Combinator::serialize.
Provided Methods§
Sourceopen spec fn wf(&self, v: Self::Type) -> bool
open spec fn wf(&self, v: Self::Type) -> bool
{ true }Well-formedness of the format [Self::type] (e.g., refinements on the type).
Sourceopen spec fn requires(&self) -> bool
open spec fn requires(&self) -> bool
{ true }Pre-conditions for parsing and serialization.
§Examples
- Sequencing combinators require that the first combinator is prefix-secure.
- Repetition combinators require that the inner combinator is prefix-secure.
crate::regular::repetition::Repeatcombinator requires that the inner combinator is productive.crate::regular::variant::Choicecombinator requires thatSndiscrate::regular::disjoint::DisjointFromFst.
Implementations on Foreign Types§
Source§impl<C: SpecCombinator> SpecCombinator for &C
impl<C: SpecCombinator> SpecCombinator for &C
Source§impl<C: SpecCombinator> SpecCombinator for Box<C>
impl<C: SpecCombinator> SpecCombinator for Box<C>
Source§impl<Fst: SecureSpecCombinator, Snd: SpecCombinator> SpecCombinator for (Fst, Snd)
impl<Fst: SecureSpecCombinator, Snd: SpecCombinator> SpecCombinator for (Fst, Snd)
Source§open spec fn requires(&self) -> bool
open spec fn requires(&self) -> bool
{ Pair::spec_new(self.0, |r: Fst::Type| self.1).requires() }Source§open spec fn wf(&self, v: Self::Type) -> bool
open spec fn wf(&self, v: Self::Type) -> bool
{ Pair::spec_new(self.0, |r: Fst::Type| self.1).wf(v) }Source§open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)>
open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)>
{ Pair::spec_new(self.0, |r: Fst::Type| self.1).spec_parse(s) }Source§open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8>
open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8>
{ Pair::spec_new(self.0, |r: Fst::Type| self.1).spec_serialize(v) }