AxiomaticMethodAttribute Class

Article
03/26/2013

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)

Usage

'Usage

Syntax

'Declaration

[AttributeUsageAttribute(AttributeTargets.Method, Inherited=false)] 
public sealed class AxiomaticMethodAttribute : Attribute

Remarks

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.

Inheritance Hierarchy

System.Object
System.Attribute
Microsoft.Modeling.AxiomaticMethodAttribute

Thread Safety

Any public static (Shared in Visual Basic) members of this type are thread safe. Any instance members are not guaranteed to be thread safe.

Platforms

Development Platforms

Microsoft Windows 7, Microsoft Windows Vista, Microsoft Windows XP SP2 or later, Microsoft Windows Server 2008, Microsoft Windows Server 2003