Description
In order to support the formal verification of higher-order functions (e.g., Option::map, Option::unwrap_or_else), it is necessary to refer to the pre-conditions and post-conditions of the closures passed as arguments within the #[thrust::requires] and #[thrust::ensures] attributes.
Currently, there is no established syntax to express that a function's correctness depends on the contract of a provided function object f.
I propose adding a syntax like f.precondition(...) and f.postcondition(...)(or a similar mechanism) to represent these contracts.
Example
#[thrust::requires(true)]#[thrust::ensures((self == std::option::Option::<T0>::None() && result == self) || (exists i:T0.self == std::option::Option::<T0>::Some(i) && ( f.precondtition(i) && exists j:T0. f.postcondition(i, j) && result == std::option::Option::<T0>::Some(j))))]pubconstfn map<U,F>(self,f:F) -> Option<U>whereF:[const]FnOnce(T) -> U + [const]Destruct,{matchself{Some(x) => Some(f(x)),None => None,}}
#[thrust::requires(true)]
#[thrust::ensures((self == std::option::Option::<T0>::None() && result == exists i:T0.
f.precondtition() && f.postcondition(i)
&& result = std::option::Option::<T0>::Some(i))
|| (exists j:T0.self == std::option::Option::<T0>::Some(j) && result == j))]pubconstfn unwrap_or_else<F>(self, f:F) -> TwhereF:[const]FnOnce() -> T + [const]Destruct,{matchself{Some(x) => x,None => f(),}}
Description
In order to support the formal verification of higher-order functions (e.g., Option::map, Option::unwrap_or_else), it is necessary to refer to the pre-conditions and post-conditions of the closures passed as arguments within the #[thrust::requires] and #[thrust::ensures] attributes.
Currently, there is no established syntax to express that a function's correctness depends on the contract of a provided function object f.
I propose adding a syntax like
f.precondition(...)andf.postcondition(...)(or a similar mechanism) to represent these contracts.Example