AxiomaticMethodAttribute Class
This API supports the exploration infrastructure and is not intended to be used directly from your code.
Namespace: Microsoft.Modeling
Assembly: Microsoft.Xrt.Runtime (in Microsoft.Xrt.Runtime.dll)
Namespace: Microsoft.Modeling
Assembly: Microsoft.Xrt.Runtime (in Microsoft.Xrt.Runtime.dll)
If static T M(T1 x1, ..., TN xn) { body } is a method tagged to be axiomatic, then it will be converted into an axiom ALL T1 x1, ..., TN xn: P1[M(x1,...,xn)] | ... | Pn[M(x1,...,xn)], where the Pi represent the path conditions with the method invocation inserted at result points.
Axiomatic methods should not refer state. They can be recursive and also mutually recursive. Applying an axiomatic method will create a symbolic value representing the application which is then subject of interpretation by the axiom, instead of yielding in actual execution.
Any public static (Shared in Visual Basic) members of this type are thread safe. Any instance members are not guaranteed to be thread safe.
Development Platforms
Microsoft Windows 7, Microsoft Windows Vista, Microsoft Windows XP SP2 or later, Microsoft Windows Server 2008, Microsoft Windows Server 2003
Community Additions
ADD
Show: