You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I would like to be able to make the serialise and deserialise functions opaque from the outside of a class implementing this trait, so that the proof does rely only on the laws. However, I'd like the functions to not be opaque inside the class definition itself.
Here for example, a class implementing the trait Serialiser should be able to see its own implementation of serialise and deserialise to prove that the laws hold. However, other classes having access to an instance of such class shouldn't be able to access the implementation details, but only the laws.
Ex:
case class CharSerialiser extends Serialiser[Char]:
def serialise(x: T): List[Char]
def deserialise(l: List[Char]): Option[T]
override def serialiseDeserialise(x: T): Boolean =
// Here the definitions are visible
deserialise(serialise(x)) == x
case class ConcatSerialiser[T, U](
ts: FixedSizeSerialiser[T],
us: FixedSizeSerialiser[U]
) extends FixedSizeSerialiser[(T, U)]:
def serialise(t: (T, U) ): List[Char] = ...
def deserialise(l: List[Char]): Option[(T, U) ] = ...
override def serialiseDeserialise(x: (T, U) ): Boolean =
// Here the implementations of ts and us should be opaque, and the proof should rely on the laws
deserialise(serialise(x)) == x
The text was updated successfully, but these errors were encountered:
when working with laws in trait, for example:
I would like to be able to make the
serialise
anddeserialise
functionsopaque
from the outside of a class implementing this trait, so that the proof does rely only on the laws. However, I'd like the functions to not beopaque
inside the class definition itself.Here for example, a class implementing the trait
Serialiser
should be able to see its own implementation ofserialise
anddeserialise
to prove that the laws hold. However, other classes having access to an instance of such class shouldn't be able to access the implementation details, but only the laws.Ex:
The text was updated successfully, but these errors were encountered: