diff --git a/.github/workflows/publish.yml b/.github/workflows/publish.yml
index 1cf6d4c..b6a6cbc 100644
--- a/.github/workflows/publish.yml
+++ b/.github/workflows/publish.yml
@@ -36,6 +36,7 @@ jobs:
dotnet-version: 10.x.x
- name: Run Unit Tests on .Net 10
+ if: github.ref == 'refs/heads/master'
run: dotnet test TestsOnly.sln -f net10.0 --verbosity quiet --filter "TestCategory!=IntegrationTest"
- name: Install GitVersion
@@ -58,6 +59,7 @@ jobs:
dotnet pack ./Configuration/AzureBlobJson/Odin.Configuration.AzureBlobJson.csproj --configuration $CONFIGURATION --output $PACKAGE_DIR
dotnet pack ./Data/SqlScriptsRunner/Odin.Data.SqlScriptsRunner.csproj --configuration $CONFIGURATION --output $PACKAGE_DIR
dotnet pack ./DesignContracts/Core/Odin.DesignContracts.csproj --configuration $CONFIGURATION --output $PACKAGE_DIR
+ dotnet pack ./DesignContracts/Tooling/Odin.DesignContracts.Tooling.csproj --configuration $CONFIGURATION --output $PACKAGE_DIR
dotnet pack ./Email/Mailgun/Odin.Email.Mailgun.csproj --configuration $CONFIGURATION --output $PACKAGE_DIR
dotnet pack ./Email/Office365/Odin.Email.Office365.csproj --configuration $CONFIGURATION --output $PACKAGE_DIR
dotnet pack ./Email/Core/Odin.Email.csproj --configuration $CONFIGURATION --output $PACKAGE_DIR
diff --git a/.gitignore b/.gitignore
index bea57b0..fe929b7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -27,7 +27,7 @@ bld/
[Oo]bj/
[Ll]og/
-# Locally provisioned build output to tools/ under DesignContracts
+# Locally provisioned tools
tools/
# Visual Studio 2015 cache/options directory
diff --git a/BackgroundProcessing/Abstractions/BackgroundProcessingProviders.cs b/BackgroundProcessing/Abstractions/BackgroundProcessingProviders.cs
index 42bb890..e72622f 100644
--- a/BackgroundProcessing/Abstractions/BackgroundProcessingProviders.cs
+++ b/BackgroundProcessing/Abstractions/BackgroundProcessingProviders.cs
@@ -1,5 +1,4 @@
-using System.Collections.Specialized;
-using Odin.System;
+using Odin.System;
namespace Odin.BackgroundProcessing
{
diff --git a/BackgroundProcessing/Abstractions/JobDetails.cs b/BackgroundProcessing/Abstractions/JobDetails.cs
index 752c865..d11ba90 100644
--- a/BackgroundProcessing/Abstractions/JobDetails.cs
+++ b/BackgroundProcessing/Abstractions/JobDetails.cs
@@ -14,7 +14,7 @@ public sealed record JobDetails
///
public JobDetails(string jobId, DateTimeOffset scheduledFor)
{
- Precondition.Requires(!string.IsNullOrWhiteSpace(jobId));
+ Contract.Requires(!string.IsNullOrWhiteSpace(jobId));
JobId = jobId;
ScheduledFor = scheduledFor;
}
diff --git a/BackgroundProcessing/Core/BackgroundProcessingOptions.cs b/BackgroundProcessing/Core/BackgroundProcessingOptions.cs
index 9e25e1f..dbb913e 100644
--- a/BackgroundProcessing/Core/BackgroundProcessingOptions.cs
+++ b/BackgroundProcessing/Core/BackgroundProcessingOptions.cs
@@ -18,7 +18,7 @@ public string Provider
get => _provider;
set
{
- Precondition.Requires(!string.IsNullOrWhiteSpace(value));
+ Contract.Requires(!string.IsNullOrWhiteSpace(value));
_provider = value.Replace("BackgroundProcessor", "", StringComparison.OrdinalIgnoreCase);
}
}
diff --git a/BackgroundProcessing/Core/DependencyInjectionExtensions.cs b/BackgroundProcessing/Core/DependencyInjectionExtensions.cs
index 27cf2d1..0cce666 100644
--- a/BackgroundProcessing/Core/DependencyInjectionExtensions.cs
+++ b/BackgroundProcessing/Core/DependencyInjectionExtensions.cs
@@ -80,7 +80,7 @@ public static void AddOdinBackgroundProcessing(
this IServiceCollection serviceCollection, IConfiguration configuration,
IConfigurationSection configurationSection, Func? sqlServerConnectionStringFactory = null)
{
- Precondition.RequiresNotNull(configurationSection);
+ Contract.RequiresNotNull(configurationSection);
BackgroundProcessingOptions options = new BackgroundProcessingOptions();
configurationSection.Bind(options);
@@ -131,8 +131,8 @@ public static void AddOdinBackgroundProcessing(
///
public static IApplicationBuilder UseBackgroundProcessing(this IApplicationBuilder app, IServiceProvider appServices)
{
- Precondition.RequiresNotNull(appServices);
- Precondition.RequiresNotNull(app);
+ Contract.RequiresNotNull(appServices);
+ Contract.RequiresNotNull(app);
BackgroundProcessingOptions options = appServices.GetRequiredService();
if (options.Provider == BackgroundProcessingProviders.Null)
@@ -142,7 +142,7 @@ public static IApplicationBuilder UseBackgroundProcessing(this IApplicationBuild
string providerAssemblyName = $"{Constants.RootNamespace}.{options.Provider}";
ResultValue serviceInjectorCreation =
- Odin.System.Activator2.TryCreate($"{providerAssemblyName}ServiceInjector",providerAssemblyName);
+ Activator2.TryCreate($"{providerAssemblyName}ServiceInjector",providerAssemblyName);
if (serviceInjectorCreation.IsSuccess)
{
diff --git a/BackgroundProcessing/Hangfire/HangfireBackgroundProcessor.cs b/BackgroundProcessing/Hangfire/HangfireBackgroundProcessor.cs
index 93bc6a9..bdb9a88 100644
--- a/BackgroundProcessing/Hangfire/HangfireBackgroundProcessor.cs
+++ b/BackgroundProcessing/Hangfire/HangfireBackgroundProcessor.cs
@@ -25,9 +25,9 @@ public sealed class HangfireBackgroundProcessor : IBackgroundProcessor
///
public HangfireBackgroundProcessor(IRecurringJobManagerV2 recurringJobManager, IBackgroundJobClient jobClient, ILoggerWrapper logger)
{
- Precondition.RequiresNotNull(recurringJobManager);
- Precondition.RequiresNotNull(jobClient);
- Precondition.RequiresNotNull(logger);
+ Contract.RequiresNotNull(recurringJobManager);
+ Contract.RequiresNotNull(jobClient);
+ Contract.RequiresNotNull(logger);
_recurringJobManager = recurringJobManager;
_jobClient = jobClient;
_logger = logger;
diff --git a/BackgroundProcessing/Hangfire/HangfirePolicyAuthorisationFilter.cs b/BackgroundProcessing/Hangfire/HangfirePolicyAuthorisationFilter.cs
index 8815666..8cc0171 100644
--- a/BackgroundProcessing/Hangfire/HangfirePolicyAuthorisationFilter.cs
+++ b/BackgroundProcessing/Hangfire/HangfirePolicyAuthorisationFilter.cs
@@ -20,7 +20,7 @@ public sealed class HangfirePolicyAuthorisationFilter : IDashboardAuthorizationF
///
public HangfirePolicyAuthorisationFilter(string policyName)
{
- Precondition.Requires(!string.IsNullOrWhiteSpace(policyName));
+ Contract.Requires(!string.IsNullOrWhiteSpace(policyName));
_policyName = policyName.Trim();
}
diff --git a/BackgroundProcessing/Hangfire/HangfireServiceInjector.cs b/BackgroundProcessing/Hangfire/HangfireServiceInjector.cs
index b7fac30..56a7317 100644
--- a/BackgroundProcessing/Hangfire/HangfireServiceInjector.cs
+++ b/BackgroundProcessing/Hangfire/HangfireServiceInjector.cs
@@ -16,8 +16,8 @@ public class HangfireServiceInjector : IBackgroundProcessorServiceInjector
public void TryAddBackgroundProcessor(IServiceCollection serviceCollection, IConfiguration configuration,
IConfigurationSection backgroundProcessingSection, Func? connectionStringFactory = null)
{
- Precondition.RequiresNotNull(serviceCollection);
- Precondition.RequiresNotNull(backgroundProcessingSection);
+ Contract.RequiresNotNull(serviceCollection);
+ Contract.RequiresNotNull(backgroundProcessingSection);
IConfigurationSection? providerSection =
backgroundProcessingSection.GetSection(BackgroundProcessingProviders.Hangfire);
if (providerSection == null)
diff --git a/Data/SqlScriptsRunner/SqlScriptsRunner.cs b/Data/SqlScriptsRunner/SqlScriptsRunner.cs
index 877122b..fd654a4 100644
--- a/Data/SqlScriptsRunner/SqlScriptsRunner.cs
+++ b/Data/SqlScriptsRunner/SqlScriptsRunner.cs
@@ -43,15 +43,15 @@ private SqlScriptsRunner(Assembly assemblyWithEmbeddedScripts)
{
// Contract.Requires(logger);
// _logger = logger;
- Precondition.Requires(assemblyWithEmbeddedScripts!=null!);
+ Contract.Requires(assemblyWithEmbeddedScripts!=null!);
_assemblyWithEmbeddedScripts = assemblyWithEmbeddedScripts!;
}
public static ResultValue CreateFromConnectionStringName(string connectionStringName,
Assembly assemblyWithEmbeddedScripts, IConfiguration configuration)
{
- Precondition.Requires(configuration!=null!);
- Precondition.Requires(assemblyWithEmbeddedScripts!=null!);
+ Contract.Requires(configuration!=null!);
+ Contract.Requires(assemblyWithEmbeddedScripts!=null!);
SqlScriptsRunner runner = new SqlScriptsRunner(assemblyWithEmbeddedScripts)
{
ConnectionString = configuration.GetConnectionString(connectionStringName)!
@@ -76,8 +76,8 @@ public static ResultValue CreateFromConnectionStringName(strin
public static ResultValue CreateFromConnectionString(string connectionString, Assembly assemblyWithEmbeddedScripts)
{
- Precondition.Requires(assemblyWithEmbeddedScripts!=null!);
- Precondition.Requires(!string.IsNullOrWhiteSpace(connectionString));
+ Contract.Requires(assemblyWithEmbeddedScripts!=null!);
+ Contract.Requires(!string.IsNullOrWhiteSpace(connectionString));
SqlScriptsRunner runner = new SqlScriptsRunner(assemblyWithEmbeddedScripts)
{
ConnectionString = connectionString
diff --git a/DesignContracts/Analyzers/PostconditionsAnalyzer.cs b/DesignContracts/Analyzers/PostconditionsAnalyzer.cs
new file mode 100644
index 0000000..72b21a7
--- /dev/null
+++ b/DesignContracts/Analyzers/PostconditionsAnalyzer.cs
@@ -0,0 +1,269 @@
+using System.Collections.Immutable;
+using Microsoft.CodeAnalysis;
+using Microsoft.CodeAnalysis.CSharp;
+using Microsoft.CodeAnalysis.CSharp.Syntax;
+using Microsoft.CodeAnalysis.Diagnostics;
+
+namespace Odin.DesignContracts.Analyzers;
+
+///
+/// Validates usage of postconditions expressed via Odin.DesignContracts.Contract.Ensures
+/// and return-value placeholders expressed via Odin.DesignContracts.Contract.Result<T>.
+///
+[DiagnosticAnalyzer(LanguageNames.CSharp)]
+public sealed class PostconditionsAnalyzer : DiagnosticAnalyzer
+{
+ ///
+ /// Postconditions must be declared in a contract block at the top of a method.
+ ///
+ public const string ContractBlockDiagnosticId = "ODIN101";
+
+ ///
+ /// Contract.Result<T> must only be used inside an Ensures condition.
+ ///
+ public const string ResultUsageDiagnosticId = "ODIN102";
+
+ ///
+ /// Postconditions are not supported for async/iterator methods (v1).
+ ///
+ public const string UnsupportedMethodDiagnosticId = "ODIN103";
+
+ ///
+ /// Postconditions require the build-time rewriter to be enabled.
+ ///
+ public const string RewriterNotEnabledDiagnosticId = "ODIN104";
+
+ ///
+ /// A contract block must be terminated by Contract.EndContractBlock() (v1).
+ ///
+ public const string MissingEndContractBlockDiagnosticId = "ODIN105";
+
+ private static readonly DiagnosticDescriptor ContractBlockRule = new(
+ ContractBlockDiagnosticId,
+ title: "Postconditions must be declared in a contract block at the start of the method",
+ messageFormat: "Postconditions must appear only at the start of the method (contract block) before any non-contract statements.",
+ category: "Usage",
+ defaultSeverity: DiagnosticSeverity.Warning,
+ isEnabledByDefault: true);
+
+ private static readonly DiagnosticDescriptor ResultUsageRule = new(
+ ResultUsageDiagnosticId,
+ title: "Contract.Result() can only be used inside a postcondition",
+ messageFormat: "Contract.Result() must only be used inside the first argument of Contract.Ensures(...).",
+ category: "Usage",
+ defaultSeverity: DiagnosticSeverity.Warning,
+ isEnabledByDefault: true);
+
+ private static readonly DiagnosticDescriptor UnsupportedMethodRule = new(
+ UnsupportedMethodDiagnosticId,
+ title: "Postconditions are not supported for async/iterator methods (v1)",
+ messageFormat: "Postconditions are not supported for this method kind (async/iterator).",
+ category: "Usage",
+ defaultSeverity: DiagnosticSeverity.Warning,
+ isEnabledByDefault: true);
+
+ private static readonly DiagnosticDescriptor RewriterNotEnabledRule = new(
+ RewriterNotEnabledDiagnosticId,
+ title: "Postconditions require the build-time rewriter",
+ messageFormat: "Postconditions are present but the Odin DesignContracts rewriter is not enabled for this project.",
+ category: "Build",
+ defaultSeverity: DiagnosticSeverity.Warning,
+ isEnabledByDefault: true);
+
+ private static readonly DiagnosticDescriptor MissingEndContractBlockRule = new(
+ MissingEndContractBlockDiagnosticId,
+ title: "Contract.EndContractBlock() is required (v1)",
+ messageFormat: "Postconditions are present but the contract block is not terminated by Contract.EndContractBlock().",
+ category: "Usage",
+ defaultSeverity: DiagnosticSeverity.Warning,
+ isEnabledByDefault: true);
+
+ ///
+ public override ImmutableArray SupportedDiagnostics =>
+ ImmutableArray.Create(ContractBlockRule, ResultUsageRule, UnsupportedMethodRule, RewriterNotEnabledRule,
+ MissingEndContractBlockRule);
+
+ ///
+ public override void Initialize(AnalysisContext context)
+ {
+ context.ConfigureGeneratedCodeAnalysis(GeneratedCodeAnalysisFlags.None);
+ context.EnableConcurrentExecution();
+ context.RegisterSyntaxNodeAction(AnalyzeMethod, SyntaxKind.MethodDeclaration);
+ }
+
+ private static void AnalyzeMethod(SyntaxNodeAnalysisContext context)
+ {
+ if (context.Node is not MethodDeclarationSyntax method)
+ return;
+
+ // Expression-bodied methods can't have a contract block.
+ if (method.ExpressionBody is not null)
+ {
+ // Still validate Result() usage if present.
+ AnalyzeResultUsage(context, method);
+ return;
+ }
+
+ if (method.Body is null)
+ return;
+
+ bool hasPostconditions = ContainsEnsuresInvocation(context, method);
+ if (!hasPostconditions)
+ {
+ // Even without Ensures, ensure Result() isn't misused.
+ AnalyzeResultUsage(context, method);
+ return;
+ }
+
+ // Enforce sync-only (v1).
+ if (method.Modifiers.Any(SyntaxKind.AsyncKeyword) || ContainsYield(method.Body))
+ {
+ context.ReportDiagnostic(Diagnostic.Create(
+ UnsupportedMethodRule,
+ method.Identifier.GetLocation()));
+ }
+
+ // Enforce contract block positioning at the top of the method.
+ bool seenNonContractStatement = false;
+ bool sawEndContractBlock = false;
+ foreach (StatementSyntax statement in method.Body.Statements)
+ {
+ if (IsContractBlockStatement(context, statement))
+ {
+ if (seenNonContractStatement)
+ {
+ context.ReportDiagnostic(Diagnostic.Create(
+ ContractBlockRule,
+ statement.GetLocation()));
+ }
+
+ if (statement is ExpressionStatementSyntax es && es.Expression is InvocationExpressionSyntax inv &&
+ IsEndContractBlockInvocation(context, inv))
+ {
+ sawEndContractBlock = true;
+ }
+ }
+ else
+ {
+ seenNonContractStatement = true;
+ }
+ }
+
+ if (!sawEndContractBlock)
+ {
+ context.ReportDiagnostic(Diagnostic.Create(
+ MissingEndContractBlockRule,
+ method.Identifier.GetLocation()));
+ }
+
+ // Ensure Result() is used only inside Ensures condition.
+ AnalyzeResultUsage(context, method);
+
+ // Require rewriter enabled when postconditions are present.
+ if (!IsRewriterEnabled(context))
+ {
+ context.ReportDiagnostic(Diagnostic.Create(
+ RewriterNotEnabledRule,
+ method.Identifier.GetLocation()));
+ }
+ }
+
+ private static bool IsRewriterEnabled(SyntaxNodeAnalysisContext context)
+ {
+ if (context.Options.AnalyzerConfigOptionsProvider.GlobalOptions
+ .TryGetValue("build_property.OdinDesignContractsRewriterEnabled", out string? enabledText))
+ {
+ return string.Equals(enabledText?.Trim(), "true", StringComparison.OrdinalIgnoreCase);
+ }
+
+ return false;
+ }
+
+ private static bool ContainsYield(BlockSyntax body)
+ => body.DescendantNodes().OfType().Any();
+
+ private static bool ContainsEnsuresInvocation(SyntaxNodeAnalysisContext context, MethodDeclarationSyntax method)
+ => method.DescendantNodes().OfType().Any(i => IsEnsuresInvocation(context, i));
+
+ private static bool IsContractBlockStatement(SyntaxNodeAnalysisContext context, StatementSyntax statement)
+ {
+ if (statement is not ExpressionStatementSyntax exprStmt)
+ return false;
+
+ if (exprStmt.Expression is not InvocationExpressionSyntax invocation)
+ return false;
+
+ return IsEnsuresInvocation(context, invocation) || IsEndContractBlockInvocation(context, invocation);
+ }
+
+ private static bool IsEnsuresInvocation(SyntaxNodeAnalysisContext context, InvocationExpressionSyntax invocation)
+ => IsContractInvocation(context, invocation, methodName: "Ensures");
+
+ private static bool IsEndContractBlockInvocation(SyntaxNodeAnalysisContext context, InvocationExpressionSyntax invocation)
+ => IsContractInvocation(context, invocation, methodName: "EndContractBlock");
+
+ private static bool IsResultInvocation(SyntaxNodeAnalysisContext context, InvocationExpressionSyntax invocation)
+ => IsContractInvocation(context, invocation, methodName: "Result");
+
+ private static bool IsContractInvocation(
+ SyntaxNodeAnalysisContext context,
+ InvocationExpressionSyntax invocation,
+ string methodName)
+ {
+ if (invocation.Expression is not MemberAccessExpressionSyntax memberAccess)
+ return false;
+
+ if (memberAccess.Name.Identifier.Text != methodName)
+ return false;
+
+ SymbolInfo symbolInfo = context.SemanticModel.GetSymbolInfo(memberAccess);
+ if (symbolInfo.Symbol is not IMethodSymbol methodSymbol)
+ return false;
+
+ if (methodSymbol.Name != methodName)
+ return false;
+
+ if (methodSymbol.ContainingType is not { Name: "Contract", ContainingNamespace: { } ns })
+ return false;
+
+ return ns.ToDisplayString() == "Odin.DesignContracts";
+ }
+
+ private static void AnalyzeResultUsage(SyntaxNodeAnalysisContext context, MethodDeclarationSyntax method)
+ {
+ foreach (InvocationExpressionSyntax invocation in method.DescendantNodes().OfType())
+ {
+ if (!IsResultInvocation(context, invocation))
+ continue;
+
+ // Must be inside: Contract.Ensures( /* condition */ ... ) - specifically inside argument #0.
+ if (!IsWithinEnsuresConditionArgument(context, invocation))
+ {
+ context.ReportDiagnostic(Diagnostic.Create(
+ ResultUsageRule,
+ invocation.GetLocation()));
+ }
+ }
+ }
+
+ private static bool IsWithinEnsuresConditionArgument(SyntaxNodeAnalysisContext context, InvocationExpressionSyntax resultInvocation)
+ {
+ // Walk up: Result() -> ... -> Argument -> ArgumentList -> Invocation (Ensures)
+ SyntaxNode? node = resultInvocation;
+ while (node is not null)
+ {
+ if (node is ArgumentSyntax arg && arg.Parent is ArgumentListSyntax argList &&
+ argList.Parent is InvocationExpressionSyntax parentInvocation &&
+ IsEnsuresInvocation(context, parentInvocation))
+ {
+ // Ensure it's the first argument.
+ int index = argList.Arguments.IndexOf(arg);
+ return index == 0;
+ }
+
+ node = node.Parent;
+ }
+
+ return false;
+ }
+}
diff --git a/DesignContracts/Core/AssemblyInfo.cs b/DesignContracts/Core/AssemblyInfo.cs
new file mode 100644
index 0000000..e20be14
--- /dev/null
+++ b/DesignContracts/Core/AssemblyInfo.cs
@@ -0,0 +1,6 @@
+using System.Runtime.CompilerServices;
+
+[assembly: InternalsVisibleTo("Tests.Odin.DesignContracts")]
+[assembly: InternalsVisibleTo("Tests.Odin.DesignContracts.Rewriter")]
+
+
diff --git a/DesignContracts/Core/Contract.cs b/DesignContracts/Core/Contract.cs
index 9f0e0bb..22c704a 100644
--- a/DesignContracts/Core/Contract.cs
+++ b/DesignContracts/Core/Contract.cs
@@ -2,7 +2,7 @@ namespace Odin.DesignContracts
{
///
/// Provides design-time contracts for runtime validation of preconditions,
- /// postconditions, and object invariants.
+ /// postconditions, class invariants, assertions and assumptions.
///
///
/// This class is intentionally similar in surface area to
@@ -11,6 +11,152 @@ namespace Odin.DesignContracts
///
public static class Contract
{
+ ///
+ /// Specifies a precondition that must hold true when the enclosing method is called.
+ ///
+ /// The precondition that is required to be true.
+ /// Optional English description of what the precondition is.
+ /// Optional pseudocode representation of the condition expression.
+ ///
+ /// Thrown when is false.
+ ///
+ public static void Requires(bool precondition, string? userMessage = null, string? conditionText = null)
+ {
+ HandleContractCondition(ContractKind.Precondition, precondition, userMessage, conditionText);
+ }
+
+ ///
+ /// Specifies a precondition that must hold true when the enclosing method is called
+ /// and throws a specific exception type when the precondition fails.
+ ///
+ ///
+ /// The type of exception to throw when the precondition fails.
+ /// The type must have a public constructor that accepts a single parameter.
+ ///
+ /// The condition that must be true.
+ /// Optional user readable message describing the precondition.
+ /// Optional user readable message describing the precondition.
+ ///
+ /// Thrown when the specified exception type cannot be constructed.
+ ///
+ ///
+ /// An instance of when is false.
+ ///
+ public static void Requires(bool precondition, string? userMessage = null,
+ string? conditionText = null)
+ where TException : Exception
+ {
+ ContractHandlingBehaviour behaviour = ContractOptions.Current.Preconditions;
+ if (behaviour == ContractHandlingBehaviour.Bypass)
+ {
+ return;
+ }
+
+ if (precondition) return;
+
+ // Try to honor the requested exception type first.
+ // Todo: Obey behaviour. Throw specific Exception only after event handling...
+ string message = BuildFailureMessage(ContractKind.Precondition, userMessage, conditionText);
+
+ Exception? exception = null;
+ try
+ {
+ exception = (Exception?)Activator.CreateInstance(typeof(TException), message);
+ }
+ catch
+ {
+ // Swallow and fall back to ContractException.
+ }
+
+ if (exception is not null)
+ {
+ throw exception;
+ }
+
+ // Fall back to standard handling if we cannot construct TException.
+ ReportFailure(behaviour, ContractKind.Precondition, userMessage, conditionText: null);
+ }
+
+ ///
+ /// Requires that argument be not null. If it is, raises an ArgumentNullException.
+ ///
+ ///
+ /// Defaults to 'Argument must not be null'
+ /// Optional pseudo-code representation of the not null expression.
+ public static void RequiresNotNull(object? argument, string? userMessage = "Argument must not be null"
+ , string? conditionText = null)
+ {
+ Requires(argument != null, userMessage, conditionText);
+ }
+
+ ///
+ /// Specifies a postcondition that must hold true when the enclosing method returns.
+ ///
+ /// The condition that must be true.
+ /// An optional message describing the postcondition.
+ /// An optional text representation of the condition expression.
+ ///
+ /// Postconditions are evaluated only when are not set to Bypass.
+ /// This method acts as a marker method for the Contracts Rewriter to instead insert calls to
+ /// ContractImplementation.Ensures() at all method returns.
+ ///
+ public static void Ensures(bool condition, string? userMessage = null, string? conditionText = null)
+ {
+ }
+
+
+ ///
+ /// Implementation of
+ ///
+ /// The condition that must be true.
+ /// An optional message describing the postcondition.
+ /// An optional text representation of the condition expression.
+ internal static void EnsuresImplementation(bool condition, string? userMessage = null, string? conditionText = null)
+ {
+ HandleContractCondition(ContractKind.Postcondition, condition, userMessage, conditionText);
+ }
+
+ ///
+ /// Specifies a condition of the class that must hold true for the class to be in a valid state.
+ ///
+ /// The condition that must be true.
+ /// An optional message describing the invariant.
+ /// An optional text representation of the condition expression.
+ public static void Invariant(bool condition, string? userMessage = null, string? conditionText = null)
+ {
+ HandleContractCondition(ContractKind.Invariant, condition, userMessage, conditionText);
+ }
+
+ ///
+ /// Specifies an assertion that must hold true at the given point in the code.
+ /// Only evaluated if ContractOptions.EnableAssertions is true.
+ ///
+ /// The condition that must be true.
+ /// An optional message describing the assertion.
+ /// An optional text representation of the condition expression.
+ ///
+ /// Assertions are always evaluated at runtime.
+ ///
+ public static void Assert(bool condition, string? userMessage = null, string? conditionText = null)
+ {
+ HandleContractCondition(ContractKind.Assertion, condition, userMessage, conditionText);
+ }
+
+ ///
+ /// Specifies an assumption that the analysis environment may rely on.
+ ///
+ /// The condition that is assumed to be true.
+ /// An optional message describing the assumption.
+ /// An optional text representation of the condition expression.
+ ///
+ /// At runtime, behaves identically to ,
+ /// but analyzers may interpret assumptions differently.
+ ///
+ public static void Assume(bool condition, string? userMessage = null, string? conditionText = null)
+ {
+ HandleContractCondition(ContractKind.Assumption, condition, userMessage, conditionText);
+ }
+
///
/// Occurs when a contract fails and before a is thrown.
///
@@ -20,40 +166,104 @@ public static class Contract
///
public static event EventHandler? ContractFailed;
- internal static void ReportFailure(ContractFailureKind kind, string? userMessage, string? conditionText)
+ internal static void ResetContractFailedEventHandlers()
{
+ ContractFailed = null;
+ }
+
+ internal static void ReportFailure(ContractHandlingBehaviour handling, ContractKind kind,
+ string? userMessage, string? conditionText)
+ {
+ // Note that if handling is inappropriately set to ByPass, then ReportFailure
+ // does nothing which is fine.
string message = BuildFailureMessage(kind, userMessage, conditionText);
- ContractFailedEventArgs args = new ContractFailedEventArgs(kind, message, userMessage, conditionText);
- ContractFailed?.Invoke(null, args);
- if (args.Handled)
+ if (handling == ContractHandlingBehaviour.EventHandlersAndEscalation ||
+ handling == ContractHandlingBehaviour.EventHandlersOnly)
{
- // A handler chose to manage the failure; do not throw by default.
- return;
+ if (ContractFailed is not null)
+ {
+ ContractFailedEventArgs args = new
+ ContractFailedEventArgs(kind, message, userMessage, conditionText);
+ ContractFailed.Invoke(null, args);
+ if (args.Handled)
+ {
+ return; // A handler chose to manage the failure; do not throw in this case...
+ }
+ }
}
- throw new ContractException(kind, message, userMessage, conditionText);
+ if (handling == ContractHandlingBehaviour.EventHandlersAndEscalation ||
+ handling == ContractHandlingBehaviour.EscalationOnly)
+ {
+ throw new ContractException(kind, message, userMessage, conditionText);
+ }
}
- internal static string BuildFailureMessage(ContractFailureKind kind, string? userMessage, string? conditionText)
+ internal static string GetKindFailedText(ContractKind kind)
{
- string kindText = kind.ToString();
-
- if (!string.IsNullOrWhiteSpace(userMessage) && !string.IsNullOrWhiteSpace(conditionText))
+ switch (kind)
{
- return $"{kindText} failed: {userMessage} [Condition: {conditionText}]";
+ case ContractKind.Precondition:
+ return "Precondition not met";
+ case ContractKind.Postcondition:
+ return "Postcondition not honoured";
+ case ContractKind.Invariant:
+ return "Invariant broken";
+ case ContractKind.Assertion:
+ return "Assertion failed";
+ case ContractKind.Assumption:
+ return "Assumption failed";
+ default:
+ throw new ArgumentOutOfRangeException(nameof(kind), kind, null);
}
+ }
- if (!string.IsNullOrWhiteSpace(userMessage))
- {
- return $"{kindText} failed: {userMessage}";
- }
+ internal static string BuildFailureMessage(ContractKind kind, string? userMessage, string? conditionText)
+ {
+ bool blankUserMessage = string.IsNullOrWhiteSpace(userMessage);
+ bool blankConditionText = string.IsNullOrWhiteSpace(conditionText);
- if (!string.IsNullOrWhiteSpace(conditionText))
- {
- return $"{kindText} failed: {conditionText}";
- }
+ if (!blankUserMessage && !blankConditionText)
+ return $"{GetKindFailedText(kind)}: {userMessage} [Condition: {conditionText}]";
+
+ if (!blankUserMessage)
+ return $"{GetKindFailedText(kind)}: {userMessage}";
+
+ if (!blankConditionText)
+ return $"{GetKindFailedText(kind)}: {conditionText}";
+
+ return $"{GetKindFailedText(kind)}.";
+ }
- return $"{kindText} failed.";
+ internal static void HandleContractCondition(ContractKind kind, bool condition, string? userMessage = null, string? conditionText = null)
+ {
+ ContractHandlingBehaviour behaviour = ContractOptions.Current.GetBehaviourFor(kind);
+ if (behaviour == ContractHandlingBehaviour.Bypass)
+ return;
+ if (!condition)
+ ReportFailure(behaviour, kind, userMessage, conditionText);
+ }
+
+
+ ///
+ /// Represents the return value of the enclosing method for use within postconditions.
+ ///
+ /// The enclosing method return type.
+ ///
+ /// The value returned by the enclosing method.
+ ///
+ ///
+ /// This API is intended to be used only inside postconditions expressed via
+ /// .
+ ///
+ /// When postconditions are enabled, it is expected that a build-time rewriter will
+ /// replace calls to this method with the actual method return value.
+ ///
+ /// Without rewriting, this method returns default.
+ ///
+ public static T Result()
+ {
+ return default!;
}
}
}
\ No newline at end of file
diff --git a/DesignContracts/Core/ContractAttributes.cs b/DesignContracts/Core/ContractAttributes.cs
index c7ac89b..e8cfe3f 100644
--- a/DesignContracts/Core/ContractAttributes.cs
+++ b/DesignContracts/Core/ContractAttributes.cs
@@ -1,29 +1,26 @@
namespace Odin.DesignContracts
{
- // ///
- // /// Identifies a method that contains class invariant checks for its declaring type.
- // ///
- // ///
- // /// Methods marked with this attribute are expected to be private, parameterless,
- // /// and to invoke for each invariant.
- // /// Source generators can use this attribute to discover and invoke invariant methods
- // /// at appropriate points (for example, at the end of constructors and public methods).
- // ///
- // [AttributeUsage(AttributeTargets.Method, Inherited = false)]
- // public sealed class ClassInvariantMethodAttribute : Attribute
- // {
- // }
- //
- // ///
- // /// Indicates that the decorated method is intended to be used only by
- // /// generated code for contract injection purposes.
- // ///
- // ///
- // /// This attribute is provided primarily as a hint to analyzers and code
- // /// generation tooling. It has no effect at runtime.
- // ///
- // [AttributeUsage(AttributeTargets.Method, Inherited = false)]
- // public sealed class ContractGeneratedMethodAttribute : Attribute
- // {
- // }
+ ///
+ /// Identifies a method that contains class invariant checks for its declaring type.
+ ///
+ ///
+ /// Methods marked with this attribute are expected to be private, parameterless,
+ /// and to invoke for each invariant.
+ /// Source generators can use this attribute to discover and invoke invariant methods
+ /// at appropriate points (for example, at the end of constructors and public methods).
+ ///
+ [AttributeUsage(AttributeTargets.Method, Inherited = false)]
+ public class ClassInvariantMethodAttribute : Attribute
+ {
+ }
+
+ ///
+ /// Methods and classes marked with this attribute can be used within calls to Contract methods. Such methods do not make any state changes.
+ ///
+ [AttributeUsage(AttributeTargets.Constructor | AttributeTargets.Method | AttributeTargets.Property |
+ AttributeTargets.Event | AttributeTargets.Delegate | AttributeTargets.Class |
+ AttributeTargets.Parameter, AllowMultiple = false, Inherited = true)]
+ public sealed class PureAttribute : Attribute
+ {
+ }
}
\ No newline at end of file
diff --git a/DesignContracts/Core/ContractException.cs b/DesignContracts/Core/ContractException.cs
index d56df52..91241a4 100644
--- a/DesignContracts/Core/ContractException.cs
+++ b/DesignContracts/Core/ContractException.cs
@@ -1,5 +1,3 @@
-using System.Runtime.Serialization;
-
namespace Odin.DesignContracts
{
///
@@ -11,7 +9,7 @@ public sealed class ContractException : Exception
///
/// Precondition, Postcondition, Invariant, Assertion or Assumption
///
- public ContractFailureKind Kind { get; }
+ public ContractKind Kind { get; }
///
/// Gets the text representation of the condition that failed, if supplied.
@@ -31,7 +29,7 @@ public sealed class ContractException : Exception
/// The user-visible message associated with the contract, if any.
/// The text representation of the condition that failed, if provided.
public ContractException(
- ContractFailureKind kind,
+ ContractKind kind,
string message,
string? userMessage = null,
string? conditionText = null)
diff --git a/DesignContracts/Core/ContractFailedEventArgs.cs b/DesignContracts/Core/ContractFailedEventArgs.cs
index 502863d..7874890 100644
--- a/DesignContracts/Core/ContractFailedEventArgs.cs
+++ b/DesignContracts/Core/ContractFailedEventArgs.cs
@@ -1,7 +1,7 @@
namespace Odin.DesignContracts
{
///
- /// Provides data for the event.
+ /// Provides data for the event.
///
public sealed class ContractFailedEventArgs : EventArgs
{
@@ -13,7 +13,7 @@ public sealed class ContractFailedEventArgs : EventArgs
/// The user-visible message associated with the contract, if any.
/// The text representation of the condition that failed, if provided.
public ContractFailedEventArgs(
- ContractFailureKind kind,
+ ContractKind kind,
string message,
string? userMessage,
string? conditionText)
@@ -27,7 +27,7 @@ public ContractFailedEventArgs(
///
/// Gets the category of the contract failure.
///
- public ContractFailureKind Kind { get; }
+ public ContractKind Kind { get; }
///
/// Gets the fully formatted failure message.
diff --git a/DesignContracts/Core/ContractFailureKind.cs b/DesignContracts/Core/ContractFailureKind.cs
deleted file mode 100644
index 43aa8a5..0000000
--- a/DesignContracts/Core/ContractFailureKind.cs
+++ /dev/null
@@ -1,34 +0,0 @@
-
-namespace Odin.DesignContracts
-{
- ///
- /// Defines the semantic category of a design contract failure.
- ///
- public enum ContractFailureKind : short
- {
- ///
- /// A precondition was broken.
- ///
- Precondition = 0,
-
- ///
- /// A postcondition was not satisfied.
- ///
- Postcondition = 1,
-
- ///
- /// A class invariant check failed.
- ///
- Invariant = 2,
-
- ///
- /// An assertion did not hold.
- ///
- Assertion = 3,
-
- ///
- /// An assumption did not hold.
- ///
- Assumption = 4
- }
-}
\ No newline at end of file
diff --git a/DesignContracts/Core/ContractKind.cs b/DesignContracts/Core/ContractKind.cs
new file mode 100644
index 0000000..1084899
--- /dev/null
+++ b/DesignContracts/Core/ContractKind.cs
@@ -0,0 +1,39 @@
+
+namespace Odin.DesignContracts
+{
+ ///
+ /// The different design contract contexts.
+ ///
+ public enum ContractKind : short
+ {
+ ///
+ /// A requirement on a class member that the client caller is
+ /// expected to honour.
+ ///
+ Precondition = 0,
+
+ ///
+ /// A requirement on a class member the member itself is expected to honour
+ /// when returning from the call.
+ ///
+ Postcondition = 1,
+
+ ///
+ /// An assertion of a condition that is expected to be true for the class
+ /// in question to be in a valid state.
+ ///
+ Invariant = 2,
+
+ ///
+ /// A condition that is simply expected to be true at any point in program execution.
+ ///
+ Assertion = 3,
+
+ ///
+ /// An assumption is stated primarily as a hint to static analysis tools
+ /// about a condition that the tool cannot deduce on its own. Assumptions
+ /// are evaluated at runtime the same as Assertions.
+ ///
+ Assumption = 4
+ }
+}
\ No newline at end of file
diff --git a/DesignContracts/Core/ContractOptions.cs b/DesignContracts/Core/ContractOptions.cs
new file mode 100644
index 0000000..f140147
--- /dev/null
+++ b/DesignContracts/Core/ContractOptions.cs
@@ -0,0 +1,193 @@
+namespace Odin.DesignContracts
+{
+ ///
+ /// Represents the configuration for runtime design contract evaluation,
+ /// provisionally exposed statically via ContractOptions.Current.
+ ///
+ ///
+ /// NOTE: Preconditions are NOT always evaluated, they can also be bypassed.
+ /// ContractOptions configuration controls the ContractHandlingBehaviour of calls
+ /// to preconditions, postconditions, invariants, assertions, and assumptions.
+ ///
+ public sealed record ContractOptions
+ {
+ ///
+ /// Configures runtime behaviour for individual precondition Requires calls.
+ ///
+ public required ContractHandlingBehaviour Preconditions { get; init; }
+
+ ///
+ /// Configures runtime behaviour for individual postcondition Ensures calls weaved into the class by the Contracts Rewriter
+ /// before each method return.
+ ///
+ public required ContractHandlingBehaviour Postconditions { get; init; }
+
+ ///
+ /// Configures runtime behaviour for individual Invariant calls in the class invariant method. In future, the intention for
+ /// setting to ByPass is that this will also bypass calling of the class invariant method entirely from every weaved invocation.
+ ///
+ public required ContractHandlingBehaviour Invariants { get; init; }
+
+ ///
+ /// Configures runtime behaviour for individual calls.
+ ///
+ public required ContractHandlingBehaviour Assumptions { get; init; }
+
+ ///
+ /// Configures runtime behaviour for individual calls.
+ ///
+ public required ContractHandlingBehaviour Assertions { get; init; }
+
+ ///
+ /// Returns the behaviour for the given contract kind.
+ ///
+ ///
+ ///
+ ///
+ public ContractHandlingBehaviour GetBehaviourFor(ContractKind kind)
+ {
+ return kind switch
+ {
+ ContractKind.Precondition => Preconditions,
+ ContractKind.Postcondition => Postconditions,
+ ContractKind.Invariant => Invariants,
+ ContractKind.Assumption => Assumptions,
+ ContractKind.Assertion => Assertions,
+ _ => throw new ArgumentOutOfRangeException(nameof(kind), kind, "Unknown contract kind")
+ };
+ }
+
+ private static ContractOptions? _current;
+
+ ///
+ /// Static facade to the current runtime instance of DesignContractOptions, which must be set
+ /// early on in application startup by calling Initialize.
+ /// Defaults to DefaultOn().
+ ///
+ ///
+ public static ContractOptions Current
+ {
+ get
+ {
+ // Temporary hack so I can continue with testing the actual rewriting...
+ // Todo: Remove and resolve configuration initialization issues.
+ if (_current is null)
+ {
+ _current = On();
+ }
+
+ return _current;
+ }
+ }
+
+ ///
+ /// Creates options with all Contract operations set to EventHandlersAndEscalation
+ ///
+ /// Enables escalation of contract violations, normally by throwing ContractExceptions.
+ /// Enables event handlers to handle contract violations.
+ ///
+ ///
+ public static ContractOptions On(bool enableEscalation = true,
+ bool enableEventHandling = true)
+ {
+ if (!enableEscalation && !enableEventHandling)
+ {
+ throw new ArgumentException(
+ $"{nameof(On)} requires enabling of either {nameof(enableEscalation)} or {nameof(enableEscalation)}.");
+ }
+
+ ContractHandlingBehaviour behaviour;
+ if (enableEscalation && enableEventHandling)
+ {
+ behaviour = ContractHandlingBehaviour.EventHandlersAndEscalation;
+ }
+ else if (enableEscalation)
+ {
+ behaviour = ContractHandlingBehaviour.EscalationOnly;
+ }
+ else
+ {
+ behaviour = ContractHandlingBehaviour.EventHandlersOnly;
+ }
+
+ return All(behaviour);
+ }
+
+
+ ///
+ /// Creates options with all Contract operations set the passed behaviour handling.
+ ///
+ /// The handling for all Contract operations.
+ ///
+ public static ContractOptions All(ContractHandlingBehaviour behaviour)
+ {
+ return new ContractOptions()
+ {
+ Invariants = behaviour,
+ Postconditions = behaviour,
+ Assertions = behaviour,
+ Assumptions = behaviour,
+ Preconditions = behaviour
+ };
+ }
+
+ ///
+ /// Creates options with all Contract operations set to Bypass,
+ /// EXCLUDING Preconditions which are handled with EventHandlersAndEscalation.
+ ///
+ ///
+ public static ContractOptions Off()
+ {
+ return new ContractOptions()
+ {
+ Invariants = ContractHandlingBehaviour.Bypass,
+ Postconditions = ContractHandlingBehaviour.Bypass,
+ Assertions = ContractHandlingBehaviour.Bypass,
+ Assumptions = ContractHandlingBehaviour.Bypass,
+ Preconditions = ContractHandlingBehaviour.EventHandlersAndEscalation
+ };
+ }
+
+ ///
+ /// Unable to understand how to get around initializing 1 static instance of Current in NUnit test runs.
+ /// throw new InvalidOperationException("Current DesignContractOptions not initialized.");
+ ///
+ ///
+ public static void Initialize(ContractOptions options)
+ => _current = options;
+
+ }
+
+ ///
+ /// Configures runtime handling for contract condition evaluation
+ /// and violation handling.
+ ///
+ public enum ContractHandlingBehaviour : short
+ {
+ ///
+ /// Skip evaluation of the contract condition entirely,
+ /// continuing program execution.
+ ///
+ Bypass,
+
+ ///
+ /// Evaluate the contract condition. If it fails,
+ /// allow any registered event handlers to handle the failure.
+ /// If no event handler marks the ContractFailedEvent as handled,
+ /// escalation is triggered, typically as the throwing of a ContractException.
+ ///
+ EventHandlersAndEscalation,
+
+ ///
+ /// Evaluate the contract condition. If it fails,
+ /// trigger escalation, typically as the throwing of a ContractException.
+ ///
+ EscalationOnly,
+
+ ///
+ /// Evaluate the contract condition. If it fails,
+ /// allow any registered event handlers to handle the failure.
+ ///
+ EventHandlersOnly
+ }
+}
\ No newline at end of file
diff --git a/DesignContracts/Core/ContractSettings.cs b/DesignContracts/Core/ContractSettings.cs
deleted file mode 100644
index 3237bca..0000000
--- a/DesignContracts/Core/ContractSettings.cs
+++ /dev/null
@@ -1,28 +0,0 @@
-// namespace Odin.DesignContracts
-// {
-// ///
-// /// Represents the configuration for runtime design contract evaluation.
-// ///
-// ///
-// /// Preconditions are always evaluated. This configuration controls the runtime
-// /// evaluation of postconditions and invariants.
-// ///
-// public sealed class ContractSettings
-// {
-// ///
-// /// Gets or sets a value indicating whether postconditions should be evaluated at runtime.
-// ///
-// ///
-// /// When false, calls to become no-ops.
-// ///
-// public bool EnablePostconditions { get; set; } = true;
-//
-// ///
-// /// Gets or sets a value indicating whether object invariants should be evaluated at runtime.
-// ///
-// ///
-// /// When false, calls to become no-ops.
-// ///
-// public bool EnableInvariants { get; set; } = true;
-// }
-// }
\ No newline at end of file
diff --git a/DesignContracts/Core/Precondition.cs b/DesignContracts/Core/Precondition.cs
deleted file mode 100644
index 9bbfe65..0000000
--- a/DesignContracts/Core/Precondition.cs
+++ /dev/null
@@ -1,80 +0,0 @@
-namespace Odin.DesignContracts;
-
-///
-/// Provides methods for runtime validation and enforcement of preconditions.
-/// These assertions are used to ensure that client callers meet the preconditions
-/// advertised as required for a given method.
-///
-public static class Precondition
-{
- ///
- /// Specifies a precondition that must hold true when the enclosing method is called.
- ///
- /// The precondition that is required to be true.
- /// Optional English description of what the precondition is.
- /// Optional pseudo-code representation of the condition expression.
- ///
- /// Thrown when is false.
- ///
- public static void Requires(bool precondition, string? userMessage = null, string? conditionText = null)
- {
- if (!precondition) Contract.ReportFailure(ContractFailureKind.Precondition, userMessage, conditionText);
- }
-
- ///
- /// Requires that argument be not null. If it is, raises an ArgumentNullException.
- ///
- ///
- /// Defaults to 'Argument must not be null'
- /// Optional pseudo-code representation of the not null expression.
- public static void RequiresNotNull(object? argument, string? userMessage = "Argument must not be null"
- , string? conditionText = null)
- {
- Requires(argument != null, userMessage, conditionText);
- }
-
- ///
- /// Specifies a precondition that must hold true when the enclosing method is called
- /// and throws a specific exception type when the precondition fails.
- ///
- ///
- /// The type of exception to throw when the precondition fails.
- /// The type must have a public constructor that accepts a single parameter.
- ///
- /// The condition that must be true.
- /// Optional user readable message describing the precondition.
- /// Optional user readable message describing the precondition.
- ///
- /// Thrown when the specified exception type cannot be constructed.
- ///
- ///
- /// An instance of when is false.
- ///
- public static void Requires(bool precondition, string? userMessage = null,
- string? conditionText = null)
- where TException : Exception
- {
- if (precondition) return;
-
- // Try to honor the requested exception type first.
- string message = Contract.BuildFailureMessage(ContractFailureKind.Precondition, userMessage, conditionText);
-
- Exception? exception = null;
- try
- {
- exception = (Exception?)Activator.CreateInstance(typeof(TException), message);
- }
- catch
- {
- // Swallow and fall back to ContractException.
- }
-
- if (exception is not null)
- {
- throw exception;
- }
-
- // Fall back to standard handling if we cannot construct TException.
- Contract.ReportFailure(ContractFailureKind.Precondition, userMessage, conditionText: null);
- }
-}
\ No newline at end of file
diff --git a/DesignContracts/CoreTests/ContractInvariantWeavingTests.cs b/DesignContracts/CoreTests/ContractInvariantWeavingTests.cs
new file mode 100644
index 0000000..0c791d6
--- /dev/null
+++ b/DesignContracts/CoreTests/ContractInvariantWeavingTests.cs
@@ -0,0 +1,59 @@
+using NUnit.Framework;
+using Odin.DesignContracts;
+using Targets;
+
+namespace Tests.Odin.DesignContracts
+{
+ [TestFixture]
+ public sealed class ContractInvariantWeavingTests
+ {
+ [SetUp]
+ public void Setup()
+ {
+ ContractOptions.Initialize(ContractOptions.All(ContractHandlingBehaviour.EscalationOnly));
+ }
+
+ [Test]
+ public void Public_constructor_has_invariant_woven_on_exit([Values] AttributeFlavour testCase)
+ {
+ ContractException? ex = Assert.Throws(() =>
+ {
+ if (testCase == AttributeFlavour.Odin)
+ {
+ new OdinInvariantTestTarget(-1);
+ }
+ else if (testCase == AttributeFlavour.BaseClassLibrary)
+ {
+ new BclInvariantTestTarget(-1);
+ }
+ });
+ AssertTestInvariantExceptionThrown(ex);
+ }
+
+ [Test]
+ public void Public_method_has_invariant_call_woven_on_entry([Values] AttributeFlavour testCase)
+ {
+ Type testTypeFor = TestSupport.GetTargetTestTypeFor(testCase);
+
+ object instance = Activator.CreateInstance(testTypeFor, 1)!;
+ TestSupport.SetPrivateField(testTypeFor, instance, "_value", -1);
+
+ Exception? ex = Assert.Catch(() =>
+ {
+ TestSupport.Invoke(testTypeFor, instance, nameof(OdinInvariantTestTarget.Increment));
+ })!;
+ AssertTestInvariantExceptionThrown(ex);
+ }
+
+ private void AssertTestInvariantExceptionThrown(Exception? ex)
+ {
+ Assert.That(ex, Is.Not.Null);
+ ContractException? contractException = ex as ContractException;
+ Assert.That(contractException, Is.Not.Null);
+ Assert.That(contractException.Kind, Is.EqualTo(ContractKind.Invariant));
+ Assert.That(contractException.UserMessage, Is.EqualTo("value must be non-negative"));
+ Assert.That(contractException.ConditionText, Is.Null);
+ Assert.That(contractException.Message, Is.EqualTo("Invariant broken: value must be non-negative"));
+ }
+ }
+}
\ No newline at end of file
diff --git a/DesignContracts/CoreTests/ContractOptionsTests.cs b/DesignContracts/CoreTests/ContractOptionsTests.cs
new file mode 100644
index 0000000..ce59b1f
--- /dev/null
+++ b/DesignContracts/CoreTests/ContractOptionsTests.cs
@@ -0,0 +1,57 @@
+using NUnit.Framework;
+using Odin.DesignContracts;
+
+namespace Tests.Odin.DesignContracts;
+
+[TestFixture]
+public class ContractOptionsTests
+{
+ [Test]
+ [TestCase(true,true, false, ContractHandlingBehaviour.EventHandlersAndEscalation)]
+ [TestCase(true,false, false, ContractHandlingBehaviour.EscalationOnly)]
+ [TestCase(false,true, false, ContractHandlingBehaviour.EventHandlersOnly)]
+ [TestCase(false,false, true, null)]
+ public void On(bool enableEscalation, bool enableEventHandlers,
+ bool invalidCombination, ContractHandlingBehaviour? expectedHandling)
+ {
+ if (invalidCombination)
+ {
+ var exception = Assert.Throws(() =>
+ ContractOptions.On(enableEscalation, enableEventHandlers));
+ Assert.That(exception.Message, Is.Not.Null);
+ return;
+ }
+
+ var sut = ContractOptions.On(enableEscalation,enableEventHandlers);
+
+ Assert.That(sut.Preconditions, Is.EqualTo(expectedHandling));
+ Assert.That(sut.Postconditions, Is.EqualTo(expectedHandling));
+ Assert.That(sut.Assertions, Is.EqualTo(expectedHandling));
+ Assert.That(sut.Assumptions, Is.EqualTo(expectedHandling));
+ Assert.That(sut.Invariants, Is.EqualTo(expectedHandling));
+ }
+
+ [Test]
+ public void Off_sets_to_Bypass()
+ {
+ ContractOptions sut = ContractOptions.Off();
+
+ Assert.That(sut.Preconditions, Is.EqualTo(ContractHandlingBehaviour.EventHandlersAndEscalation));
+ Assert.That(sut.Postconditions, Is.EqualTo(ContractHandlingBehaviour.Bypass));
+ Assert.That(sut.Assertions, Is.EqualTo(ContractHandlingBehaviour.Bypass));
+ Assert.That(sut.Assumptions, Is.EqualTo(ContractHandlingBehaviour.Bypass));
+ Assert.That(sut.Invariants, Is.EqualTo(ContractHandlingBehaviour.Bypass));
+ }
+
+ [Test]
+ public void All_sets_everything([Values] ContractHandlingBehaviour handling)
+ {
+ var sut = ContractOptions.All(handling);
+
+ Assert.That(sut.Preconditions, Is.EqualTo(handling));
+ Assert.That(sut.Postconditions, Is.EqualTo(handling));
+ Assert.That(sut.Assertions, Is.EqualTo(handling));
+ Assert.That(sut.Assumptions, Is.EqualTo(handling));
+ Assert.That(sut.Invariants, Is.EqualTo(handling));
+ }
+}
\ No newline at end of file
diff --git a/DesignContracts/CoreTests/ContractTests.cs b/DesignContracts/CoreTests/ContractTests.cs
new file mode 100644
index 0000000..57d53ba
--- /dev/null
+++ b/DesignContracts/CoreTests/ContractTests.cs
@@ -0,0 +1,178 @@
+using NUnit.Framework;
+using Odin.DesignContracts;
+
+namespace Tests.Odin.DesignContracts
+{
+ [TestFixture]
+ public sealed class ContractTests
+ {
+ [Test]
+ public void Contract_failure_handling_depends_on_configured_behaviours(
+ [Values] ContractHandlingBehaviour behaviour, [Values] ContractKind kind)
+ {
+ ContractOptions.Initialize(ContractOptions.All(behaviour));
+
+ AssertConfiguredHandlingFor(kind, behaviour);
+ if (behaviour == ContractHandlingBehaviour.Bypass | behaviour == ContractHandlingBehaviour.EventHandlersOnly)
+ {
+ Assert.DoesNotThrow(() =>
+ Contract.HandleContractCondition(kind, false, "userMessage", "conditionText"));
+ }
+ else
+ {
+ ContractException? ex = Assert.Throws(() =>
+ Contract.HandleContractCondition(kind, false, "userMessage", "conditionText"));
+ Assert.That(ex, Is.Not.Null);
+ Assert.That(ex!.Message, Contains.Substring("userMessage"));
+ Assert.That(ex!.Message, Contains.Substring("conditionText"));
+ }
+ }
+
+ [Test]
+ [TestCase(ContractHandlingBehaviour.Bypass, false, false)]
+ [TestCase(ContractHandlingBehaviour.EscalationOnly, false, true)]
+ [TestCase(ContractHandlingBehaviour.EventHandlersOnly, true, false)]
+ [TestCase(ContractHandlingBehaviour.EventHandlersAndEscalation, true, false)]
+ public void Contract_handling_fires_ContractFailed_delegates_depending_on_configured_behaviour(
+ ContractHandlingBehaviour behaviour, bool handlerShouldFire, bool exceptionShouldBeThrown)
+ {
+ ContractOptions.Initialize(ContractOptions.All(behaviour));
+ foreach (ContractKind kind in AllKinds())
+ {
+ AssertConfiguredHandlingFor(kind, behaviour);
+ bool handlerFiredFlag = false;
+ EventHandler handler = (sender, args) =>
+ {
+ handlerFiredFlag = true;
+ args.Handled = true;
+ };
+ Contract.ContractFailed += handler;
+
+ if (exceptionShouldBeThrown)
+ {
+ Assert.Throws(() =>
+ Contract.HandleContractCondition(kind, false, "userMessage", "conditionText"));
+ }
+ else
+ {
+ Contract.HandleContractCondition(kind, false, "userMessage", "conditionText");
+ }
+
+ Assert.That(handlerFiredFlag, Is.EqualTo(handlerShouldFire));
+ Contract.ContractFailed -= handler;
+ }
+ }
+
+ [Test]
+ [Description("For EventHandlersAndEscalation the event handler can set the Handled property")]
+ public void Contract_event_handler_can_handle_contract_failure(
+ [Values] ContractKind kind, [Values] bool handleFailure)
+ {
+ ContractOptions.Initialize(ContractOptions.All(ContractHandlingBehaviour.EventHandlersAndEscalation));
+ AssertConfiguredHandlingFor(kind, ContractHandlingBehaviour.EventHandlersAndEscalation);
+ bool exceptionShouldBeThrown = !handleFailure;
+ EventHandler handler = (sender, args) =>
+ {
+ args.Handled = handleFailure;
+ };
+ Contract.ContractFailed += handler;
+
+ if (exceptionShouldBeThrown)
+ {
+ Assert.Throws(() =>
+ Contract.HandleContractCondition(kind, false, "msg"));
+ }
+ else
+ {
+ Assert.DoesNotThrow(() =>
+ Contract.HandleContractCondition(kind, false, "msg"));
+ }
+
+ Contract.ContractFailed -= handler;
+ }
+
+ [Test]
+ [TestCase("userMessage", "conditionText", "{0}: userMessage [Condition: conditionText]")]
+ [TestCase("userMessage", " ", "{0}: userMessage")]
+ [TestCase("userMessage", null, "{0}: userMessage")]
+ [TestCase("userMessage", "", "{0}: userMessage")]
+ [TestCase("", "", "{0}.")]
+ [TestCase("", null, "{0}.")]
+ [TestCase(" ", null, "{0}.")]
+ [TestCase(null, null, "{0}.")]
+ [TestCase(null, "", "{0}.")]
+ [TestCase(null, " ", "{0}.")]
+ [TestCase(null, "conditionText", "{0}: conditionText")]
+ [TestCase("", "conditionText", "{0}: conditionText")]
+ [TestCase(" ", "conditionText", "{0}: conditionText")]
+ public void Escalation_exception_message_formatting(string? userMessage, string? conditionText,
+ string messageFormat)
+ {
+ ContractOptions.Initialize(ContractOptions.On());
+ foreach (ContractKind kind in AllKinds())
+ {
+ string messageExpected = string.Format(messageFormat, Contract.GetKindFailedText(kind));
+ ContractException? ex = Assert.Throws(() =>
+ Contract.HandleContractCondition(kind, false, userMessage, conditionText));
+ Assert.That(ex, Is.Not.Null);
+ Assert.That(ex!.Message, Is.EqualTo(messageExpected), "Exception message is incorrect");
+ }
+ }
+
+ [Test]
+ public void Handle_does_not_escalate_on_success([Values] ContractHandlingBehaviour handlingBehaviour)
+ {
+ ContractOptions.Initialize(ContractOptions.All(handlingBehaviour));
+
+ AssertConfiguredHandlingFor(ContractKind.Precondition, handlingBehaviour);
+ Assert.DoesNotThrow(() => Contract.Requires(true, "Message"));
+ Assert.DoesNotThrow(() => Contract.Requires(true, "Message"));
+ AssertConfiguredHandlingFor(ContractKind.Postcondition, handlingBehaviour);
+ Assert.DoesNotThrow(() => Contract.EnsuresImplementation(true, "Message"));
+ AssertConfiguredHandlingFor(ContractKind.Invariant, handlingBehaviour);
+ Assert.DoesNotThrow(() => Contract.Invariant(true, "Message"));
+ AssertConfiguredHandlingFor(ContractKind.Assumption, handlingBehaviour);
+ Assert.DoesNotThrow(() => Contract.Assume(true, "Message"));
+ AssertConfiguredHandlingFor(ContractKind.Assertion, handlingBehaviour);
+ Assert.DoesNotThrow(() => Contract.Assert(true, "Message"));
+ }
+
+ [Test]
+ public void Requires_not_null_throws_contract_exception_if_argument_null()
+ {
+ ContractOptions.Initialize(ContractOptions.On());
+
+ ContractException? exception = Assert.Throws(() =>
+ Contract.RequiresNotNull(null as string, "myArg is required."));
+
+ Assert.That(exception, Is.Not.Null);
+ Assert.That(exception!.Message, Is.EqualTo("Precondition not met: myArg is required."));
+ Assert.That(exception.UserMessage, Is.EqualTo("myArg is required."));
+ }
+
+ internal void AssertConfiguredHandlingFor(ContractKind kind, ContractHandlingBehaviour handlingBehaviour)
+ {
+ Assert.That(ContractOptions.Current.GetBehaviourFor(kind), Is.EqualTo(handlingBehaviour), $"Expected {kind} handling to be {handlingBehaviour}");
+ }
+
+ internal ContractKind[] AllKinds()
+ {
+ return Enum.GetValues();
+ }
+ }
+
+ [TestFixture(typeof(ArgumentNullException))]
+ [TestFixture(typeof(ArgumentException))]
+ [TestFixture(typeof(DivideByZeroException))]
+ public sealed class ContractRequiresOfTExceptionTests where TException : Exception
+ {
+ [Test]
+ public void Requires_of_T_throws_specific_exception()
+ {
+ TException? ex = Assert.Throws(() => Contract.Requires(false, "msg"));
+
+ Assert.That(ex, Is.Not.Null);
+ Assert.That(ex, Is.InstanceOf());
+ }
+ }
+}
\ No newline at end of file
diff --git a/DesignContracts/CoreTests/TestSupport.cs b/DesignContracts/CoreTests/TestSupport.cs
new file mode 100644
index 0000000..3a11b03
--- /dev/null
+++ b/DesignContracts/CoreTests/TestSupport.cs
@@ -0,0 +1,52 @@
+using System.Reflection;
+using Targets;
+
+namespace Tests.Odin.DesignContracts;
+
+public enum AttributeFlavour
+{
+ Odin,
+ BaseClassLibrary
+}
+
+public static class TestSupport
+{
+ public static Type GetTargetTestTypeFor(AttributeFlavour testCase)
+ {
+ if (testCase == AttributeFlavour.Odin)
+ {
+ return typeof(OdinInvariantTestTarget);
+ }
+
+ if (testCase == AttributeFlavour.BaseClassLibrary)
+ {
+ return typeof(BclInvariantTestTarget);
+ }
+
+ throw new NotSupportedException(testCase.ToString());
+ }
+
+ public static void SetPrivateField(Type declaringType, object instance, string fieldName, object? value)
+ {
+ FieldInfo f = declaringType.GetField(fieldName, BindingFlags.Instance | BindingFlags.NonPublic)
+ ?? throw new InvalidOperationException($"Missing field '{fieldName}'.");
+ f.SetValue(instance, value);
+ }
+
+ public static object? Invoke(Type declaringType, object instance, string methodName)
+ {
+ MethodInfo m = declaringType.GetMethod(methodName, BindingFlags.Instance | BindingFlags.Public)
+ ?? throw new InvalidOperationException($"Missing method '{methodName}'.");
+ try
+ {
+ return m.Invoke(instance, null);
+ }
+ catch (TargetInvocationException tie) when (tie.InnerException is not null)
+ {
+ throw tie.InnerException;
+ }
+ }
+
+}
+
+
diff --git a/DesignContracts/Tests/Tests.Odin.DesignContracts.csproj b/DesignContracts/CoreTests/Tests.Odin.DesignContracts.csproj
similarity index 72%
rename from DesignContracts/Tests/Tests.Odin.DesignContracts.csproj
rename to DesignContracts/CoreTests/Tests.Odin.DesignContracts.csproj
index a951a29..914fc43 100644
--- a/DesignContracts/Tests/Tests.Odin.DesignContracts.csproj
+++ b/DesignContracts/CoreTests/Tests.Odin.DesignContracts.csproj
@@ -2,7 +2,8 @@
net8.0;net9.0;net10.0
enable
- Tests.Odin.DesignContracts
+ Tests where the target classes under test HAVE been weaved in post build
+ by the Design-by-Contract tooling.
true
true
1591;
@@ -16,7 +17,7 @@
-
+
-
\ No newline at end of file
+
diff --git a/DesignContracts/README.md b/DesignContracts/README.md
new file mode 100644
index 0000000..076a81b
--- /dev/null
+++ b/DesignContracts/README.md
@@ -0,0 +1,69 @@
+# Odin.DesignContracts (Design by Contract)
+
+This repository includes a lightweight Design-by-Contract runtime in [`DesignContracts/Core/Contract.cs`](Core/Contract.cs:1) plus tooling to support **postconditions** (Ensures) by rewriting compiled IL.
+
+## Why IL rewriting (and not source generators)
+
+Roslyn **source generators** can only *add* new source; they cannot rewrite an existing method body to:
+
+- capture a return value, and
+- run postconditions on **every** exit path.
+
+To support Code-Contracts-style authoring such as `Contract.Ensures(Contract.Result() != null)` we use a build-time IL rewriter.
+
+## Postconditions (v1)
+
+Postconditions are declared with [`Contract.Ensures()`](Core/Contract-New.cs:41) and may refer to the enclosing method return value via [`Contract.Result()`](Core/Contract-New.cs:13).
+
+### Authoring rules (v1)
+
+- Postconditions must appear in a **contract block** at the start of a method.
+- The contract block must be terminated with [`Contract.EndContractBlock()`](Core/Contract-New.cs:31).
+- Sync methods only (no `async`, no iterators) in v1.
+
+Example:
+
+```csharp
+using Odin.DesignContracts;
+
+public static string GetName(User user)
+{
+ Contract.Requires(user is not null);
+
+ Contract.Ensures(Contract.Result() is not null);
+ Contract.EndContractBlock();
+
+ return user.Name;
+}
+```
+
+At build time the rewriter injects the `Ensures(...)` checks immediately before method exit, after capturing the return value.
+
+### Runtime enable/disable
+
+`Ensures` checks are gated by `ContractRuntime.PostconditionsEnabled` (see [`ContractRuntime`](Core/ContractRuntime.cs:1)). When disabled, postconditions are a no-op.
+
+## Object invariants (v1)
+
+Object invariants are authored by declaring a private, parameterless, `void` method marked with
+[`ContractInvariantMethodAttribute`](Core/ContractAttributes.cs:1), and calling
+[`Contract.Invariant()`](Core/Contract-New.cs:68) inside that method.
+
+At build time the IL rewriter wires up invariant execution as follows:
+
+- If a type declares exactly one invariant method (either `Odin.DesignContracts.ContractInvariantMethodAttribute`
+ or `System.Diagnostics.Contracts.ContractInvariantMethodAttribute`), the rewriter injects calls to that invariant method
+ at **entry and exit** of all **public instance** methods and **public instance** property accessors.
+- Public instance constructors (`.ctor`) get invariant calls at **exit only**.
+- Any public method/property accessor marked `[System.Diagnostics.Contracts.Pure]` is **excluded** from invariant weaving.
+
+Invariant checks are gated by `ContractRuntime.InvariantsEnabled`.
+
+## Tooling package
+
+The meta-package [`Odin.DesignContracts.Tooling`](Tooling/Odin.DesignContracts.Tooling.csproj:1) is responsible for:
+
+- shipping analyzers (to validate authoring), and
+- running the IL rewriter after compilation via `buildTransitive` targets.
+
+The IL rewriter implementation lives in [`DesignContracts/Rewriter/Program.cs`](Rewriter/Program.cs:1).
diff --git a/DesignContracts/Rewriter/AssemblyInfo.cs b/DesignContracts/Rewriter/AssemblyInfo.cs
new file mode 100644
index 0000000..e8ea779
--- /dev/null
+++ b/DesignContracts/Rewriter/AssemblyInfo.cs
@@ -0,0 +1,4 @@
+using System.Runtime.CompilerServices;
+
+[assembly: InternalsVisibleTo("Tests.Odin.DesignContracts.Rewriter")]
+
diff --git a/DesignContracts/Rewriter/AssemblyRewriter.cs b/DesignContracts/Rewriter/AssemblyRewriter.cs
new file mode 100644
index 0000000..060b4ee
--- /dev/null
+++ b/DesignContracts/Rewriter/AssemblyRewriter.cs
@@ -0,0 +1,108 @@
+using Microsoft.Build.Framework;
+using Mono.Cecil;
+
+namespace Odin.DesignContracts.Rewriter;
+
+///
+/// Handles Design-by-Contract rewriting of a given assembly.
+///
+internal class AssemblyRewriter
+{
+ ///
+ /// Constructor
+ ///
+ /// The input assembly path,
+ /// typically in the 'intermediate build output' under the 'obj' folder.
+ ///
+ /// If omitted, defaults to 'InputAssembly.odin-design-contracts-weaved.dll'
+ /// in the same folder as the input assembly.
+ /// Thrown if the assembly to rewrite does not exist.
+ internal AssemblyRewriter(string targetAssemblyPath, ILoggingAdaptor logger,
+ string? alternativeOutputPath = null)
+ {
+ TargetAssemblyPath = targetAssemblyPath;
+ _logger = logger;
+ AlternativeOutputPath = alternativeOutputPath;
+
+ if (!File.Exists(TargetAssemblyPath))
+ {
+ var msg = $"Assembly not found: {TargetAssemblyPath}";
+ _logger.LogMessage(LogImportance.High,msg);
+ throw new FileNotFoundException(msg);
+ }
+ }
+
+ private readonly ILoggingAdaptor _logger;
+
+ ///
+ /// The assembly to rewrite. Note that if OutputPath is specified,
+ /// the rewritten assembly is saved to OutputPath, else the assembly located
+ /// as TargetPath is overwritten after a call to Rewrite()
+ ///
+ internal string TargetAssemblyPath { get; }
+
+ internal string TargetAssemblyPdbPath
+ => Path.ChangeExtension(TargetAssemblyPath, ".pdb");
+
+ ///
+ /// Optional alternative path that the rewritten assembly should be written to,
+ /// else TargetAssemblyPath is overwritten by default.
+ ///
+ internal string? AlternativeOutputPath { get; }
+
+ private string GetOutputPath()
+ => AlternativeOutputPath ?? TargetAssemblyPath;
+
+ ///
+ /// Writes invariants and postconditions into the assembly at TargetPath,
+ /// or OutputPath if specified.
+ ///
+ internal void Rewrite()
+ {
+ string assemblyDir = Path.GetDirectoryName(Path.GetFullPath(TargetAssemblyPath))!;
+ DefaultAssemblyResolver resolver = new();
+ resolver.AddSearchDirectory(assemblyDir);
+
+ // Debug symbols in a .pdb file may or may not be present.
+ // We'll read them via a stream if present to ensure no issues when
+ ReaderParameters readerParameters;
+ bool symbolsPresent = File.Exists(TargetAssemblyPdbPath);
+ if (symbolsPresent)
+ {
+ MemoryStream symbolStream = new MemoryStream(File.ReadAllBytes(TargetAssemblyPdbPath));
+ symbolStream.Seek(0, SeekOrigin.Begin);
+ readerParameters = new()
+ {
+ AssemblyResolver = resolver,
+ ReadSymbols = true,
+ SymbolStream = symbolStream
+ };
+ }
+ else
+ {
+ readerParameters = new()
+ {
+ AssemblyResolver = resolver,
+ ReadSymbols = false
+ };
+ }
+
+ // Read the bytes into memory first to fully decouple the reader from the file on disk.
+ using MemoryStream ms = new MemoryStream(File.ReadAllBytes(TargetAssemblyPath));
+ using AssemblyDefinition assembly = AssemblyDefinition.ReadAssembly(ms, readerParameters);
+ int rewritten = 0;
+ foreach (ModuleDefinition module in assembly.Modules)
+ {
+ foreach (TypeDefinition type in module.GetTypes())
+ {
+ TypeRewriter currentType = new(type, _logger);
+ rewritten += currentType.Rewrite();
+ }
+ }
+ WriterParameters writerParameters = new()
+ {
+ WriteSymbols = symbolsPresent
+ };
+ assembly.Write(GetOutputPath(), writerParameters);
+ }
+}
\ No newline at end of file
diff --git a/DesignContracts/Rewriter/CecilExtensions.cs b/DesignContracts/Rewriter/CecilExtensions.cs
new file mode 100644
index 0000000..4fc29cc
--- /dev/null
+++ b/DesignContracts/Rewriter/CecilExtensions.cs
@@ -0,0 +1,55 @@
+using Mono.Cecil;
+using Mono.Cecil.Cil;
+
+namespace Odin.DesignContracts.Rewriter;
+
+internal static class CecilExtensions
+{
+ internal static bool HasAnyAttributeIn(this ICustomAttributeProvider provider, string[] attributeFullNames)
+ => provider.HasCustomAttributes && provider.CustomAttributes.Any(a => attributeFullNames.Contains(a.AttributeType.FullName));
+
+ internal static bool HasAttribute(this ICustomAttributeProvider provider, string attributeFullName)
+ => provider.HasCustomAttributes && provider.CustomAttributes.Any(a => a.AttributeType.FullName == attributeFullName);
+
+ public static bool IsPure(TypeDefinition declaringType, MethodDefinition method)
+ {
+ if (method.HasAnyAttributeIn(Names.PureAttributeFullNames))
+ return true;
+
+ // For accessors, also honour [Pure] on the property itself.
+ if (method.IsGetter || method.IsSetter)
+ {
+ PropertyDefinition? prop = declaringType.Properties.FirstOrDefault(p => p.GetMethod == method || p.SetMethod == method);
+ if (prop is not null && prop.HasAnyAttributeIn(Names.PureAttributeFullNames))
+ return true;
+ }
+ return false;
+ }
+
+ public static Instruction CloneInstruction(this Instruction instruction)
+ {
+ // Minimal cloning sufficient for contract block statements.
+ // We intentionally do not support cloning branch targets / exception handler operands in v1.
+ if (instruction.Operand is null)
+ return Instruction.Create(instruction.OpCode);
+
+ return instruction.Operand switch
+ {
+ sbyte b => Instruction.Create(instruction.OpCode, b),
+ byte b => Instruction.Create(instruction.OpCode, (sbyte)b), // Cecil uses sbyte for short forms.
+ int i => Instruction.Create(instruction.OpCode, i),
+ long l => Instruction.Create(instruction.OpCode, l),
+ float f => Instruction.Create(instruction.OpCode, f),
+ double d => Instruction.Create(instruction.OpCode, d),
+ string s => Instruction.Create(instruction.OpCode, s),
+ MethodReference mr => Instruction.Create(instruction.OpCode, mr),
+ FieldReference fr => Instruction.Create(instruction.OpCode, fr),
+ TypeReference tr => Instruction.Create(instruction.OpCode, tr),
+ ParameterDefinition pd => Instruction.Create(instruction.OpCode, pd),
+ VariableDefinition vd => Instruction.Create(instruction.OpCode, vd),
+ _ => throw new NotSupportedException(
+ $"Unsupported operand type in contract block cloning: {instruction.Operand.GetType().FullName} (opcode {instruction.OpCode}).")
+ };
+ }
+
+}
\ No newline at end of file
diff --git a/DesignContracts/Rewriter/ConsoleLoggingAdaptor.cs b/DesignContracts/Rewriter/ConsoleLoggingAdaptor.cs
new file mode 100644
index 0000000..28d6e9b
--- /dev/null
+++ b/DesignContracts/Rewriter/ConsoleLoggingAdaptor.cs
@@ -0,0 +1,36 @@
+using Microsoft.Build.Framework;
+
+namespace Odin.DesignContracts.Rewriter;
+
+///
+public class ConsoleLoggingAdaptor : ILoggingAdaptor
+{
+ ///
+ public void LogMessage(LogImportance importance, string? message, params object[] messageArgs)
+ {
+ Console.WriteLine(message, messageArgs);
+ if (importance == LogImportance.High)
+ {
+ Console.Error.WriteLine(message, messageArgs);
+ }
+ else if (importance == LogImportance.Normal)
+ {
+ Console.WriteLine(message, messageArgs);
+ }
+ // Don't write Low diagnostic messages to the console
+ }
+
+ ///
+ public void LogMessage(string? subcategory, string? code, string? helpKeyword, string? file, int lineNumber, int columnNumber,
+ int endLineNumber, int endColumnNumber, LogImportance importance, string? message, params object[] messageArgs)
+ {
+ LogMessage(importance, message, messageArgs);
+ }
+
+ ///
+ public void LogErrorFromException(Exception exception, bool showStackTrace, bool showDetail, string file)
+ {
+ Console.WriteLine(exception.Message);
+
+ }
+}
\ No newline at end of file
diff --git a/DesignContracts/Rewriter/ILoggingAdaptor.cs b/DesignContracts/Rewriter/ILoggingAdaptor.cs
new file mode 100644
index 0000000..a5dd1ff
--- /dev/null
+++ b/DesignContracts/Rewriter/ILoggingAdaptor.cs
@@ -0,0 +1,82 @@
+namespace Odin.DesignContracts.Rewriter;
+
+///
+/// This is to avoid needing to ship Microsoft.Build.Framework assemblies
+/// with the tooling if we want to use MSBuild LogImportance directly.
+///
+public enum LogImportance
+{
+ ///
+ /// High importance messages
+ ///
+ High,
+ ///
+ /// Normal importance messages
+ ///
+ Normal,
+ ///
+ /// Low importance messages
+ ///
+ Low
+}
+
+///
+/// Created so that AssemblyRewriter can log to console or MSBuild output.
+///
+public interface ILoggingAdaptor
+{
+ ///
+ /// Logs a message of the given importance using the specified string.
+ /// Thread safe.
+ ///
+ ///
+ /// Take care to order the parameters correctly or the other overload will be called inadvertently.
+ ///
+ /// Log verbosity level of the message.
+ /// The message string.
+ /// Optional arguments for formatting the message string.
+ /// Thrown when message is null.
+ public void LogMessage(LogImportance importance, string? message, params object[] messageArgs);
+
+
+ ///
+ /// Logs a message using the specified string and other message details.
+ /// Thread safe.
+ ///
+ /// Description of the warning type (can be null).
+ /// Message code (can be null)
+ /// The help keyword for the host IDE (can be null).
+ /// The path to the file causing the message (can be null).
+ /// The line in the file causing the message (set to zero if not available).
+ /// The column in the file causing the message (set to zero if not available).
+ /// The last line of a range of lines in the file causing the message (set to zero if not available).
+ /// The last column of a range of columns in the file causing the message (set to zero if not available).
+ /// Importance of the message.
+ /// The message string.
+ /// Optional arguments for formatting the message string.
+ /// Thrown when message is null.
+ public void LogMessage(
+ string? subcategory,
+ string? code,
+ string? helpKeyword,
+ string? file,
+ int lineNumber,
+ int columnNumber,
+ int endLineNumber,
+ int endColumnNumber,
+ LogImportance importance,
+ string? message,
+ params object[] messageArgs);
+
+ ///
+ /// Logs an error using the message, and optionally the stack-trace from the given exception, and
+ /// optionally inner exceptions too.
+ /// Thread safe.
+ ///
+ /// Exception to log.
+ /// If true, callstack will be appended to message.
+ /// Whether to log exception types and any inner exceptions.
+ /// File related to the exception, or null if the project file should be logged
+ /// Thrown when exception is null.
+ public void LogErrorFromException(Exception exception, bool showStackTrace, bool showDetail, string file);
+}
\ No newline at end of file
diff --git a/DesignContracts/Rewriter/MethodRewriter.cs b/DesignContracts/Rewriter/MethodRewriter.cs
new file mode 100644
index 0000000..99de2a8
--- /dev/null
+++ b/DesignContracts/Rewriter/MethodRewriter.cs
@@ -0,0 +1,290 @@
+using Microsoft.Build.Framework;
+using Mono.Cecil;
+using Mono.Cecil.Cil;
+using Mono.Cecil.Rocks;
+
+namespace Odin.DesignContracts.Rewriter;
+
+///
+/// Handles Design-by-Contract rewriting of a given type member,
+/// including methods, property accessors and constructors.
+///
+internal class MethodRewriter
+{
+ private readonly TypeRewriter _parentRewriter;
+
+ public MethodRewriter(MethodDefinition method, TypeRewriter parentRewriter)
+ {
+ Method = method;
+ _parentRewriter = parentRewriter;
+ }
+
+ public MethodDefinition Method { get; }
+
+ ///
+ /// Rewrites the type member returning true if any contract rewrites
+ /// were needed, and false if none were required.
+ ///
+ ///
+ public bool Rewrite()
+ {
+ // Only handle sync (v1). We rely on analyzers to enforce this, but be defensive.
+ // if (method.IsAsync)
+ // return false;
+
+ // What about properties? Surely these can have no body?
+ if (!Method.HasBody) return false;
+
+ Method.Body.SimplifyMacros();
+
+ MethodWeavingResult weaving = new MethodWeavingResult(IsInvariantToBeWeaved(), TryFindPostconditionInstructions());
+
+ if (weaving.NothingToWeave)
+ {
+ // Nothing to do.
+ Method.Body.OptimizeMacros();
+ return false;
+ }
+
+ ILProcessor il = Method.Body.GetILProcessor();
+
+ // Inject invariant call at entry (before any user code).
+ if (weaving.Invariant.OnEntry)
+ {
+ // An instructionless member body is possible... I suppose the member could have been stubbed.
+ Instruction first = Method.Body.Instructions.FirstOrDefault() ?? Instruction.Create(OpCodes.Nop);
+ if (Method.Body.Instructions.Count == 0)
+ il.Append(first);
+
+ InsertInvariantCallBefore(il, first, _parentRewriter.InvariantMethod!);
+ }
+
+ // Remove the postconditions from the method when postconditions are present.
+ // We could skip this as Contract.Ensures are all simply no-ops...?
+ foreach (Instruction instruction in weaving.PostconditionsToWeave)
+ {
+ // If the instruction was already removed as part of a previous remove, skip.
+ if (Method.Body.Instructions.Contains(instruction))
+ il.Remove(instruction);
+ }
+
+ // If we need to inject postconditions and/or invariant calls at exit, do it per-return.
+ // Todo: If there are multiple returns, create a shadow method to execute the
+ // invariant and\or postconditions, calling it from each return.
+ if (weaving.OnExitWeavingRequired)
+ {
+ VariableDefinition? resultVar = null;
+ bool isVoid = IsVoidReturnType();
+ if (!isVoid)
+ {
+ resultVar = new VariableDefinition(Method.ReturnType);
+ Method.Body.Variables.Add(resultVar);
+ Method.Body.InitLocals = true;
+ }
+
+ List returns = Method.Body.Instructions.Where(i => i.OpCode == OpCodes.Ret).ToList();
+ foreach (Instruction returnInst in returns)
+ {
+ // For non-void methods we must preserve the return value while we call extra code.
+ if (!isVoid)
+ {
+ il.InsertBefore(returnInst, Instruction.Create(OpCodes.Stloc, resultVar!));
+ }
+
+
+ foreach (Instruction inst in weaving.PostconditionsToWeave)
+ {
+ Instruction cloned = inst.CloneInstruction();
+
+ if (!isVoid && IsResultCall(cloned))
+ {
+ // Replace call Contract.Result() with ldloc resultVar.
+ cloned = Instruction.Create(OpCodes.Ldloc, resultVar!);
+ }
+
+ il.InsertBefore(returnInst, cloned);
+ }
+
+ if (weaving.Invariant.OnExit)
+ {
+ InsertInvariantCallBefore(il, returnInst, _parentRewriter.InvariantMethod!);
+ }
+
+ if (!isVoid)
+ {
+ il.InsertBefore(returnInst, Instruction.Create(OpCodes.Ldloc, resultVar!));
+ }
+ }
+ }
+ Method.Body.OptimizeMacros();
+
+ string invariantResult;
+ if (weaving.Invariant.BothEntryAndExit)
+ {
+ invariantResult = " invariant calls (entry & exit)";
+ }
+ else if (weaving.Invariant.NeitherEntryNorExit)
+ {
+ invariantResult = "";
+ }
+ else
+ {
+ invariantResult = weaving.Invariant.OnEntry ? " invariant call (on entry)" : " invariant call (on exit)";
+ }
+ string postconditionResult = weaving.PostconditionsToWeave.Any() ? " postcondition calls" : "";
+ if (invariantResult!="" && postconditionResult!="") postconditionResult=" and " + postconditionResult;
+ string message = $"Weaved{invariantResult}{postconditionResult} into {Method.Name} of type {_parentRewriter.Type.FullName}.";
+ _parentRewriter.Logger.LogMessage(LogImportance.Low, message);
+ return true;
+ }
+
+ public InvariantWeavingResult IsInvariantToBeWeaved()
+ {
+ bool canWeaveInvariant = _parentRewriter.HasInvariant && IsPublicInstanceMethod();
+ bool isInvariantMethodItself = _parentRewriter.InvariantMethod is not null && Method == _parentRewriter.InvariantMethod;
+
+ // Per requirements:
+ // - Constructors: invariants at exit only
+ // - Other public instance methods + public instance property accessors: invariants at entry and exit
+
+ bool weaveInvariantOnEntry = canWeaveInvariant && !isInvariantMethodItself && !IsInstanceConstructor();
+ bool weaveInvariantOnExit = canWeaveInvariant && !isInvariantMethodItself;
+
+ // Exclude [Pure] methods and [Pure] properties (for accessors).
+ // Ignore [Pure] on constructors...
+ if (!IsInstanceConstructor() && weaveInvariantOnEntry && IsPure())
+ {
+ weaveInvariantOnEntry = false;
+ weaveInvariantOnExit = false;
+ }
+
+ return new InvariantWeavingResult()
+ {
+ OnEntry = weaveInvariantOnEntry,
+ OnExit = weaveInvariantOnExit
+ };
+ }
+
+ ///
+ /// Returns any postcondition Ensures() instruction calls found.
+ ///
+ ///
+ public List TryFindPostconditionInstructions()
+ {
+ // For V1 we will attempt to simply extract any Postcondition.Ensures()
+ // calls from the method body if they exist. I am a total noob at IL so have no clue
+ // about finding and moving postcondition calls inside conditionals.
+ // Another v1 option would be to require all postconditions to be before a postcondition contract block,
+ // and then preconditions after that.
+ List postconditionEnsuresCalls = new List();
+
+ IList instructions = Method.Body.Instructions;
+ if (instructions.Count == 0)
+ return postconditionEnsuresCalls;
+
+ for (int i = 0; i < instructions.Count; i++)
+ {
+ Instruction inst = instructions[i];
+ if (IsPostconditionEnsuresCall(inst))
+ {
+ postconditionEnsuresCalls.Add(inst);
+ }
+ }
+
+ return postconditionEnsuresCalls;
+ }
+
+ public static bool IsPostconditionEnsuresCall(Instruction inst)
+ => IsStaticCallToPostconditionMethod(inst, "Ensures");
+
+ public static bool IsResultCall(Instruction inst)
+ => IsStaticCallToPostconditionMethod(inst, "Result");
+
+ public static bool IsStaticCallToPostconditionMethod(Instruction inst, string methodName)
+ {
+ if (inst.OpCode != OpCodes.Call)
+ return false;
+
+ if (inst.Operand is not MethodReference mr)
+ return false;
+
+ if (mr.Name != methodName)
+ return false;
+
+ // Handle generic instance method as well.
+ string declaringType = mr.DeclaringType.FullName;
+ return declaringType == Names.OdinPostconditionEnsuresTypeFullName;
+ }
+
+ ///
+ /// True if Method is a public instance method.
+ ///
+ ///
+ public bool IsPublicInstanceMethod()
+ {
+ return Method is { IsPublic: true, IsStatic: false };
+ }
+
+ ///
+ /// True if Method is marked as [Pure] or if it is a property accessor of a [Pure] property.
+ ///
+ ///
+ public bool IsPure()
+ {
+ if (Method.HasAnyAttributeIn(Names.PureAttributeFullNames))
+ return true;
+
+ // For accessors, also honour [Pure] on the property itself.
+ if (Method.IsGetter || Method.IsSetter)
+ {
+ PropertyDefinition? prop = _parentRewriter.Type.Properties.FirstOrDefault(p => p.GetMethod == Method || p.SetMethod == Method);
+ if (prop is not null && prop.HasAnyAttributeIn(Names.PureAttributeFullNames))
+ return true;
+ }
+
+ return false;
+ }
+
+ ///
+ /// True if Method returns void.
+ ///
+ ///
+ public bool IsVoidReturnType()
+ {
+ return Method.ReturnType.MetadataType == MetadataType.Void;
+ }
+
+ public bool IsInstanceConstructor()
+ {
+ return Method.IsConstructor && !Method.IsStatic;
+ }
+
+ private void InsertInvariantCallBefore(ILProcessor il, Instruction before, MethodDefinition invariantMethod)
+ {
+ // instance.Invariant();
+ il.InsertBefore(before, Instruction.Create(OpCodes.Ldarg_0));
+ il.InsertBefore(before, Instruction.Create(OpCodes.Call, invariantMethod));
+ }
+
+ internal record InvariantWeavingResult
+ {
+ public required bool OnEntry { get; init; }
+ public required bool OnExit { get; init; }
+ public bool BothEntryAndExit => OnEntry && OnExit;
+ public bool NeitherEntryNorExit => !OnEntry && !OnExit;
+ }
+
+ internal record MethodWeavingResult
+ {
+ public MethodWeavingResult(InvariantWeavingResult invariant, List postconditionsFound)
+ {
+ Invariant = invariant;
+ PostconditionsToWeave = postconditionsFound;
+ }
+ public InvariantWeavingResult Invariant { get; }
+ public List PostconditionsToWeave { get; }
+ public bool NothingToWeave => !PostconditionsToWeave.Any() && !Invariant.OnEntry && !Invariant.OnExit;
+ public bool OnExitWeavingRequired => PostconditionsToWeave.Any() || Invariant.OnExit;
+ }
+
+}
\ No newline at end of file
diff --git a/DesignContracts/Rewriter/MsBuildLoggingAdaptor.cs b/DesignContracts/Rewriter/MsBuildLoggingAdaptor.cs
new file mode 100644
index 0000000..4beee65
--- /dev/null
+++ b/DesignContracts/Rewriter/MsBuildLoggingAdaptor.cs
@@ -0,0 +1,54 @@
+using Microsoft.Build.Framework;
+using Microsoft.Build.Utilities;
+
+namespace Odin.DesignContracts.Rewriter;
+
+///
+public class MsBuildLoggingAdaptor : ILoggingAdaptor
+{
+ private readonly TaskLoggingHelper _msBuildLogger;
+
+ ///
+ /// Constructor
+ ///
+ ///
+ public MsBuildLoggingAdaptor(TaskLoggingHelper msBuildLogger)
+ {
+ _msBuildLogger = msBuildLogger;
+ }
+
+ ///
+ public void LogMessage(LogImportance importance, string? message, params object[] messageArgs)
+ {
+ _msBuildLogger.LogMessage(MapImportance(importance), message, messageArgs);
+ }
+
+ ///
+ public void LogMessage(string? subcategory, string? code, string? helpKeyword, string? file, int lineNumber, int columnNumber,
+ int endLineNumber, int endColumnNumber, LogImportance importance, string? message, params object[] messageArgs)
+ {
+ _msBuildLogger.LogMessage(subcategory, code, helpKeyword, file, lineNumber, columnNumber, endLineNumber,
+ endColumnNumber, MapImportance(importance), message, messageArgs);
+ }
+
+ private MessageImportance MapImportance(LogImportance importance)
+ {
+ switch (importance)
+ {
+ case LogImportance.High:
+ return MessageImportance.High;
+ case LogImportance.Normal:
+ return MessageImportance.Normal;
+ case LogImportance.Low:
+ return MessageImportance.Low;
+ default:
+ throw new ArgumentOutOfRangeException(nameof(importance), importance, null);
+ }
+ }
+
+ ///
+ public void LogErrorFromException(Exception exception, bool showStackTrace, bool showDetail, string file)
+ {
+ _msBuildLogger.LogErrorFromException(exception, showStackTrace, showDetail, file);
+ }
+}
\ No newline at end of file
diff --git a/DesignContracts/Rewriter/Names.cs b/DesignContracts/Rewriter/Names.cs
new file mode 100644
index 0000000..57e6618
--- /dev/null
+++ b/DesignContracts/Rewriter/Names.cs
@@ -0,0 +1,18 @@
+namespace Odin.DesignContracts.Rewriter;
+
+///
+/// Full names of all the attributes used in Design Contracts
+///
+internal static class Names
+{
+ internal const string BclContractNamespace = "System.Diagnostics.Contracts";
+ internal const string OdinDesignContractsNamespace = "Odin.DesignContracts";
+ internal const string OdinPostconditionEnsuresTypeFullName = OdinDesignContractsNamespace + ".Contract";
+ internal const string OdinDesignContractsRewriter = OdinDesignContractsNamespace + ".Rewriter";
+ internal const string OdinInvariantAttributeFullName = OdinDesignContractsNamespace + ".ClassInvariantMethodAttribute";
+ internal const string BclInvariantAttributeFullName = BclContractNamespace + ".ContractInvariantMethodAttribute";
+ internal const string OdinPureAttributeFullName = OdinDesignContractsNamespace + ".PureAttribute";
+ internal const string BclPureAttributeFullName = BclContractNamespace + ".PureAttribute";
+ internal static readonly string[] PureAttributeFullNames = [OdinPureAttributeFullName, BclPureAttributeFullName];
+ internal static readonly string[] InvariantAttributeFullNames = [OdinInvariantAttributeFullName, BclInvariantAttributeFullName];
+}
\ No newline at end of file
diff --git a/DesignContracts/Rewriter/Odin.DesignContracts.Rewriter.csproj b/DesignContracts/Rewriter/Odin.DesignContracts.Rewriter.csproj
new file mode 100644
index 0000000..9a7a514
--- /dev/null
+++ b/DesignContracts/Rewriter/Odin.DesignContracts.Rewriter.csproj
@@ -0,0 +1,16 @@
+
+
+ Exe
+ net8.0;net9.0;net10.0
+ true
+ enable
+ Odin.DesignContracts.Rewriter
+ 1591;1573;
+
+
+
+
+
+
+
+
diff --git a/DesignContracts/Rewriter/Program.cs b/DesignContracts/Rewriter/Program.cs
new file mode 100644
index 0000000..e92a313
--- /dev/null
+++ b/DesignContracts/Rewriter/Program.cs
@@ -0,0 +1,52 @@
+using Microsoft.Build.Framework;
+
+namespace Odin.DesignContracts.Rewriter;
+
+///
+/// Build-time IL rewriter that injects Design-by-Contract postconditions into method exit paths,
+/// as well as Design-by-Contract class invariant calls at both entry to and exit from all
+/// public members on the API surface, unless marked 'Pure'.
+///
+internal static class Program
+{
+ private static int Main(string[] args)
+ {
+ if (args.Length < 1)
+ {
+ Console.Error.WriteLine($"{Names.OdinDesignContractsRewriter}: Usage 'dotnet {Names.OdinDesignContractsRewriter}.dll '");
+ return 3;
+ }
+
+ string assemblyPath = args[0];
+ string? outputPath = null;
+ if (args.Length >= 2)
+ {
+ outputPath = args[1];
+ }
+
+ if (!File.Exists(assemblyPath))
+ {
+ Console.Error.WriteLine($"{Names.OdinDesignContractsRewriter}: Input assembly not found: {assemblyPath}");
+ return 2;
+ }
+
+ var logger = new ConsoleLoggingAdaptor();
+ try
+ {
+ AssemblyRewriter contractsRewriter = new AssemblyRewriter(assemblyPath, logger,outputPath);
+ contractsRewriter.Rewrite();
+ return 0;
+ }
+ catch (Exception ex)
+ {
+ logger.LogMessage(LogImportance.High,$"{Names.OdinDesignContractsRewriter}: Unexpected error while rewriting assembly..." );
+ logger.LogErrorFromException(ex, true, true,assemblyPath);
+ return 1;
+ }
+ }
+
+
+
+
+
+}
\ No newline at end of file
diff --git a/DesignContracts/Rewriter/TypeRewriter.cs b/DesignContracts/Rewriter/TypeRewriter.cs
new file mode 100644
index 0000000..1921335
--- /dev/null
+++ b/DesignContracts/Rewriter/TypeRewriter.cs
@@ -0,0 +1,109 @@
+using Microsoft.Build.Framework;
+using Mono.Cecil;
+
+namespace Odin.DesignContracts.Rewriter;
+
+///
+/// Handles Design-by-Contract rewriting of a given type.
+///
+internal class TypeRewriter
+{
+ private readonly TypeDefinition _target;
+ private MethodDefinition? _invariant;
+ private bool _invariantSearched = false;
+ private ILoggingAdaptor _logger;
+
+ ///
+ /// Constructor
+ ///
+ ///
+ ///
+ internal TypeRewriter(TypeDefinition target, ILoggingAdaptor logger)
+ {
+ if (target == null!) throw new ArgumentNullException(nameof(target));
+ _target = target;
+ _logger = logger;
+ }
+
+ ///
+ /// The enclosed Type being handled.
+ ///
+ internal TypeDefinition Type => _target;
+
+ internal ILoggingAdaptor Logger => _logger;
+
+ internal bool HasInvariant => InvariantMethod!=null;
+
+ ///
+ /// Null if none was found.
+ ///
+ internal MethodDefinition? InvariantMethod
+ {
+ get
+ {
+ if (!_invariantSearched)
+ {
+ FindInvariantMethodOrThrow();
+ }
+ return _invariant;
+ }
+ }
+
+ ///
+ /// Rewrites the type returning the number of members rewritten.
+ ///
+ ///
+ internal int Rewrite()
+ {
+ int rewritten = 0;
+ foreach (var member in GetMembersToTryRewrite())
+ {
+ if (!member.Rewrite())
+ continue;
+ rewritten++;
+ }
+ return rewritten;
+ }
+
+ internal IReadOnlyList GetMembersToTryRewrite()
+ {
+ return _target.Methods.Select(c => new MethodRewriter(c,this)).ToList();
+ }
+
+ internal void FindInvariantMethodOrThrow()
+ {
+ List candidates = _target.Methods
+ .Where(m => m.HasAnyAttributeIn(Names.InvariantAttributeFullNames))
+ .ToList();
+
+ _invariantSearched = true;
+
+ if (candidates.Count == 0)
+ return;
+
+ if (candidates.Count > 1)
+ {
+ throw new InvalidOperationException(
+ $"Type '{_target.FullName}' has multiple invariant methods. " +
+ $"Exactly 1 method may be marked with either of: {string.Join(" | ", Names.InvariantAttributeFullNames)}.");
+ }
+
+ MethodDefinition invariant = candidates[0];
+
+ if (invariant.IsStatic)
+ throw new InvalidOperationException($"Invariant method must be an instance method: {invariant.FullName}");
+
+ if (invariant.Parameters.Count != 0)
+ throw new InvalidOperationException($"Invariant method must be parameterless: {invariant.FullName}");
+
+ if (invariant.ReturnType.MetadataType != MetadataType.Void)
+ throw new InvalidOperationException($"Invariant method must return void: {invariant.FullName}");
+
+ if (!invariant.HasBody)
+ throw new InvalidOperationException($"Invariant method must have a body: {invariant.FullName}");
+
+ _logger.LogMessage(LogImportance.Low, $"Found invariant method: {invariant.FullName} to weave for type {_target.FullName}.");
+ _invariant = invariant;
+ }
+
+}
\ No newline at end of file
diff --git a/DesignContracts/Rewriter/WeaveDesignContracts.cs b/DesignContracts/Rewriter/WeaveDesignContracts.cs
new file mode 100644
index 0000000..03ad4db
--- /dev/null
+++ b/DesignContracts/Rewriter/WeaveDesignContracts.cs
@@ -0,0 +1,37 @@
+using Microsoft.Build.Framework;
+
+namespace Odin.DesignContracts.Rewriter;
+
+///
+/// MSBuild task for running the Design-by-Contract rewriter.
+///
+public class WeaveDesignContracts : Microsoft.Build.Utilities.Task
+{
+ ///
+ /// Runs the Design-by-Contract rewriter on the assembly to rewrite.
+ ///
+ ///
+ public override bool Execute()
+ {
+ var logger = new MsBuildLoggingAdaptor(Log);
+ try
+ {
+ AssemblyRewriter contractsRewriter = new AssemblyRewriter(AssemblyToRewritePath, logger);
+ contractsRewriter.Rewrite();
+ return true;
+ }
+ catch (Exception err)
+ {
+ Log.LogMessage(MessageImportance.High,$"{Names.OdinDesignContractsNamespace}: Unhandled error while rewriting assembly {AssemblyToRewritePath}.");
+ Log.LogErrorFromException(err,true,true,AssemblyToRewritePath);
+ return false;
+ }
+
+ }
+
+ ///
+ /// Path to the assembly to be rewritten.
+ ///
+ [Required]
+ public string AssemblyToRewritePath { get; set; }
+}
\ No newline at end of file
diff --git a/DesignContracts/RewriterTests/CecilAssemblyContext.cs b/DesignContracts/RewriterTests/CecilAssemblyContext.cs
new file mode 100644
index 0000000..1195d4c
--- /dev/null
+++ b/DesignContracts/RewriterTests/CecilAssemblyContext.cs
@@ -0,0 +1,62 @@
+using System.Reflection;
+using Mono.Cecil;
+using Targets;
+
+namespace Tests.Odin.DesignContracts.Rewriter;
+
+///
+/// Encapsulates access to a Cecil Assembly context for a given assembly for testing...
+///
+internal sealed class CecilAssemblyContext : IDisposable
+{
+ public AssemblyDefinition Assembly { get; }
+
+ public static CecilAssemblyContext GetTargetsUntooledAssemblyContext()
+ {
+ return new CecilAssemblyContext(typeof(OdinInvariantTestTarget).Assembly);
+ }
+
+ public CecilAssemblyContext(Assembly sourceAssembly)
+ {
+ string assemblyPath = sourceAssembly.Location;
+ string assemblyDir = Path.GetDirectoryName(Path.GetFullPath(sourceAssembly.Location))!;
+ DefaultAssemblyResolver resolver = new();
+ resolver.AddSearchDirectory(assemblyDir);
+ ReaderParameters readerParameters = new()
+ {
+ AssemblyResolver = resolver,
+ ReadSymbols = File.Exists(Path.ChangeExtension(assemblyPath, ".pdb")),
+ };
+
+ Assembly = AssemblyDefinition.ReadAssembly(assemblyPath, readerParameters);
+ }
+
+ public TypeDefinition? FindType(string fullName)
+ {
+ return AllTypes.FirstOrDefault(t => t.FullName == fullName);
+ }
+
+ public TypeDefinition? FindType(string nameSpace, string typeName)
+ {
+ return FindType($"{nameSpace}.{typeName}");
+ }
+
+ private List? _allTypes;
+ public IReadOnlyList AllTypes
+ {
+ get
+ {
+ if (_allTypes == null)
+ {
+ _allTypes = Assembly.Modules.SelectMany(m => m.GetTypes()).ToList();
+ }
+ return _allTypes;
+ }
+ }
+
+ public void Dispose()
+ {
+ Assembly.Dispose();
+ }
+
+}
\ No newline at end of file
diff --git a/DesignContracts/RewriterTests/MethodRewriterTests.cs b/DesignContracts/RewriterTests/MethodRewriterTests.cs
new file mode 100644
index 0000000..03f3d6d
--- /dev/null
+++ b/DesignContracts/RewriterTests/MethodRewriterTests.cs
@@ -0,0 +1,34 @@
+using Mono.Cecil;
+using Moq;
+using NUnit.Framework;
+using Odin.DesignContracts.Rewriter;
+using Targets;
+
+namespace Tests.Odin.DesignContracts.Rewriter;
+
+[TestFixture]
+public sealed class MethodRewriterTests
+{
+ [Test]
+ [TestCase(typeof(OdinInvariantTestTarget),"get_" + nameof(OdinInvariantTestTarget.PureProperty), true)]
+ [TestCase(typeof(BclInvariantTestTarget), "get_" + nameof(BclInvariantTestTarget.PureProperty),true)]
+ [TestCase(typeof(BclInvariantTestTarget), nameof(BclInvariantTestTarget.PureGetValue),true)]
+ [TestCase(typeof(BclInvariantTestTarget), "get_" + nameof(BclInvariantTestTarget.NonPureProperty),false)]
+ public void Pure_methods_are_recognised(Type type, string methodName, bool isPure)
+ {
+ CecilAssemblyContext context = CecilAssemblyContext.GetTargetsUntooledAssemblyContext();
+ MethodRewriter? sut = GetMethodHandlerFor(context, type, methodName);
+
+ Assert.That(sut, Is.Not.Null);
+ Assert.That(sut!.IsPure, Is.EqualTo(isPure));
+ }
+
+ private MethodRewriter? GetMethodHandlerFor(CecilAssemblyContext context, Type type, string methodName)
+ {
+ TypeDefinition? typeDef = context.FindType(type.FullName!);
+ TypeRewriter rewriter = new TypeRewriter(typeDef!, new Mock().Object);
+ MethodDefinition? def = rewriter.Type.Methods.FirstOrDefault(n => n.Name == methodName);
+ return new MethodRewriter(def!, rewriter);
+ }
+
+}
diff --git a/DesignContracts/RewriterTests/RewriterTests.cs b/DesignContracts/RewriterTests/RewriterTests.cs
new file mode 100644
index 0000000..e8684d6
--- /dev/null
+++ b/DesignContracts/RewriterTests/RewriterTests.cs
@@ -0,0 +1,313 @@
+using System.Diagnostics.Contracts;
+using System.Reflection;
+using Mono.Cecil;
+using Moq;
+using NUnit.Framework;
+using Odin.DesignContracts;
+using Odin.DesignContracts.Rewriter;
+using Targets;
+
+namespace Tests.Odin.DesignContracts.Rewriter;
+
+[TestFixture]
+public sealed class RewriterTests
+{
+ [SetUp]
+ public void SetUp()
+ {
+ // Ensure invariants are enabled even if the test environment sets env vars.
+ ContractOptions.Initialize(ContractOptions.On());
+ }
+
+ [Test]
+ public void Public_constructor_runs_invariant_on_exit([Values] AttributeFlavour testCase)
+ {
+ Type targetType = GetTargetTestTypeFor(testCase);
+ using RewrittenAssemblyContext context = new RewrittenAssemblyContext(targetType.Assembly);
+ Assert.That(ContractOptions.Current.Invariants, Is.EqualTo(ContractHandlingBehaviour.EventHandlersAndEscalation));
+ Assert.That(ContractOptions.Current.Postconditions, Is.EqualTo(ContractHandlingBehaviour.EventHandlersAndEscalation));
+
+ Type t = context.GetTypeOrThrow(targetType.FullName!);
+
+ //
+ Exception? exception = Assert.Catch(() =>
+ {
+ try
+ {
+ Activator.CreateInstance(t, -1);
+ }
+ catch (TargetInvocationException tie) when (tie.InnerException is not null)
+ {
+ throw tie.InnerException;
+ }
+ });
+ Assert.That(exception, Is.Not.Null);
+ Assert.That(exception!.Message, Is.EqualTo("Invariant broken: value must be non-negative"));
+ }
+
+ [Test]
+ [Description("Increment would only cause an Invariant exception at method entry, as at exit value = 0 would satisfy the invariant.")]
+ public void Public_method_runs_invariant_on_entry([Values] AttributeFlavour testCase)
+ {
+ Type targetType = GetTargetTestTypeFor(testCase);
+ using RewrittenAssemblyContext context = new RewrittenAssemblyContext(targetType.Assembly);
+ Type t = context.GetTypeOrThrow(targetType.FullName!);
+
+ object instance = Activator.CreateInstance(t, 1)!;
+ TestSupport.SetPrivateField(t, instance, "_value", -1);
+
+ Exception? ex = Assert.Catch(() => { TestSupport.Invoke(t, instance, nameof(OdinInvariantTestTarget.Increment)); })!;
+
+ Assert.That(ex, Is.Not.Null);
+ Assert.That(ex.Message, Contains.Substring("Invariant broken:"));
+ }
+
+ [Test]
+ [Description("MakeInvalid would only cause an Invariant exception at method exit, not entry.")]
+ public void Public_method_runs_invariant_on_exit([Values] AttributeFlavour testCase)
+ {
+ Type targetType = GetTargetTestTypeFor(testCase);
+ using RewrittenAssemblyContext context = new RewrittenAssemblyContext(targetType.Assembly);
+ Type t = context.GetTypeOrThrow(targetType.FullName!);
+
+ object instance = Activator.CreateInstance(t, 1)!;
+
+ Exception? ex = Assert.Catch(() => { TestSupport.Invoke(t, instance, nameof(OdinInvariantTestTarget.MakeInvalid)); })!;
+
+ Assert.That(ex, Is.Not.Null);
+ Assert.That(ex.Message, Contains.Substring("Invariant broken:"));
+ }
+
+ [Test]
+ public void Pure_method_is_excluded_from_invariant_weaving([Values] AttributeFlavour testCase)
+ {
+ Type targetType = GetTargetTestTypeFor(testCase);
+ using RewrittenAssemblyContext context = new RewrittenAssemblyContext(targetType.Assembly);
+ Type t = context.GetTypeOrThrow(targetType.FullName!);
+
+ object instance = Activator.CreateInstance(t, 1)!;
+ TestSupport.SetPrivateField(t, instance, "_value", -1);
+
+ // If [Pure] is honoured, this returns the invalid value without invariant checks throwing.
+ object? result = TestSupport.Invoke(t, instance, "PureGetValue");
+
+ Assert.That(result, Is.EqualTo(-1));
+ }
+
+ [Test]
+ public void Pure_property_is_excluded_from_invariant_weaving([Values] AttributeFlavour testCase)
+ {
+ Type targetType = GetTargetTestTypeFor(testCase);
+ using RewrittenAssemblyContext context = new RewrittenAssemblyContext(targetType.Assembly);
+ Type t = context.GetTypeOrThrow(targetType.FullName!);
+
+ object instance = Activator.CreateInstance(t, 1)!;
+ TestSupport.SetPrivateField(t, instance, "_value", -1);
+
+ object? value = TestSupport.Invoke(t, instance, "get_PureProperty");
+
+ Assert.That(value, Is.EqualTo(-1));
+ }
+
+ [Test]
+ public void Non_pure_property_is_woven_and_checks_invariants([Values] AttributeFlavour testCase)
+ {
+ Type targetType = GetTargetTestTypeFor(testCase);
+ using RewrittenAssemblyContext context = new RewrittenAssemblyContext(targetType.Assembly);
+ Type t = context.GetTypeOrThrow(targetType.FullName!);
+
+ object instance = Activator.CreateInstance(t, 1)!;
+ TestSupport.SetPrivateField(t, instance, "_value", -1);
+
+ PropertyInfo p = t.GetProperty("NonPureProperty")!;
+
+ Exception? ex = Assert.Catch(() =>
+ {
+ try
+ {
+ _ = p.GetValue(instance);
+ }
+ catch (TargetInvocationException tie) when (tie.InnerException is not null)
+ {
+ throw tie.InnerException;
+ }
+ })!;
+ Assert.That(ex, Is.Not.Null);
+ Assert.That(ex.Message, Contains.Substring("Invariant broken:"));
+ }
+
+ [Test]
+ public void Multiple_invariant_methods_causes_rewrite_to_fail([Values] AttributeFlavour firstInvariantFlavour,
+ [Values] AttributeFlavour secondInvariantFlavour)
+ {
+ // Arrange: create a temp copy of this test assembly and inject a second [ClassInvariantMethod].
+ Type firstType = GetTargetTestTypeFor(firstInvariantFlavour);
+ Type invariantAttributeTestCaseType = GetClassInvariantAttributeTypeFor(firstInvariantFlavour);
+
+ string originalPath = firstType.Assembly.Location;
+ using TempDirectory temp = new TempDirectory();
+
+ string inputPath = Path.Combine(temp.Path, Path.GetFileName(originalPath));
+ File.Copy(originalPath, inputPath, overwrite: true);
+
+ // Read the bytes into memory first to fully decouple the reader from the file on disk.
+ byte[] assemblyBytes = File.ReadAllBytes(inputPath);
+ using (MemoryStream ms = new MemoryStream(assemblyBytes))
+ using (AssemblyDefinition assemblyDefinition = AssemblyDefinition.ReadAssembly(ms,
+ new ReaderParameters { ReadWrite = false, ReadingMode = ReadingMode.Immediate }))
+ {
+ TypeDefinition targetType = assemblyDefinition.MainModule.GetType(firstType.FullName!)
+ ?? throw new InvalidOperationException("Failed to locate target type in temp assembly.");
+
+ MethodDefinition increment = targetType.Methods
+ .First(m => m.Name == nameof(OdinInvariantTestTarget.Increment));
+
+ // Add a second invariant attribute to a different method.
+ ConstructorInfo ctor = invariantAttributeTestCaseType.GetConstructor(Type.EmptyTypes)
+ ?? throw new InvalidOperationException("Invariant attribute must have a parameterless ctor.");
+ MethodReference? ctorRef = assemblyDefinition.MainModule.ImportReference(ctor);
+ increment.CustomAttributes.Add(new CustomAttribute(ctorRef));
+
+ assemblyDefinition.Write(inputPath);
+ }
+
+ // Act + Assert
+ string outputPath = Path.Combine(temp.Path, "out.dll");
+ InvalidOperationException? expectedError = Assert.Throws(() =>
+ new AssemblyRewriter(inputPath, new Mock().Object, outputPath).Rewrite());
+ Assert.That(expectedError, Is.Not.Null);
+ }
+
+ [Test]
+ [TestCase(3, true)]
+ [TestCase(13, false)]
+ public void Requires_throws_if_condition_broken(int testValue, bool shouldThrow)
+ {
+ OdinInvariantTestTarget sut = new OdinInvariantTestTarget(1);
+
+ if (shouldThrow)
+ {
+ Exception? exception = Assert.Catch(() => sut.RequiresYGreaterThan10(testValue));
+ Assert.That(exception, Is.Not.Null);
+ Assert.That(exception, Is.InstanceOf());
+ ContractException ex = (ContractException)exception!;
+ Assert.That(ex!.Kind, Is.EqualTo(ContractKind.Precondition));
+ Assert.That(ex.Message, Is.EqualTo("Precondition not met: y must be greater than 10"));
+ }
+ else
+ {
+ Assert.DoesNotThrow(() => sut.RequiresYGreaterThan10(testValue));
+ }
+ }
+
+ [Test]
+ [TestCase(3, true)]
+ [TestCase(13, false)]
+ public void Assert_throws_if_condition_broken(int testValue, bool shouldThrow)
+ {
+ OdinInvariantTestTarget sut = new OdinInvariantTestTarget(1);
+
+ if (shouldThrow)
+ {
+ Exception? exception = Assert.Catch(() => sut.AssertYGreaterThan10(testValue));
+ Assert.That(exception, Is.Not.Null);
+ Assert.That(exception, Is.InstanceOf());
+ ContractException ex = (ContractException)exception!;
+ Assert.That(ex!.Kind, Is.EqualTo(ContractKind.Assertion));
+ Assert.That(ex.Message, Is.EqualTo("Assertion failed: y must be greater than 10"));
+ }
+ else
+ {
+ Assert.DoesNotThrow(() => sut.AssertYGreaterThan10(testValue));
+ }
+ }
+
+ [Test]
+ [TestCase(3, true)]
+ [TestCase(13, false)]
+ public void Assume_throws_if_condition_broken(int testValue, bool shouldThrow)
+ {
+ OdinInvariantTestTarget sut = new OdinInvariantTestTarget(1);
+
+ if (shouldThrow)
+ {
+ Exception? exception = Assert.Catch(() => sut.AssumeYGreaterThan10(testValue));
+ Assert.That(exception, Is.Not.Null);
+ Assert.That(exception, Is.InstanceOf());
+ ContractException ex = (ContractException)exception!;
+ Assert.That(ex!.Kind, Is.EqualTo(ContractKind.Assumption));
+ Assert.That(ex.Message, Is.EqualTo("Assumption failed: y must be greater than 10"));
+ }
+ else
+ {
+ Assert.DoesNotThrow(() => sut.AssumeYGreaterThan10(testValue));
+ }
+ }
+
+
+ [Test]
+ public void Single_postcondition_is_woven([Values("VoidSingleConditionSingleReturn")] string methodName,
+ [Values(-1, 1)] int testNumber)
+ {
+ bool exceptionExpected = testNumber < 0;
+ Type targetUnwrittenType = typeof(PostconditionsTestTarget);
+ using RewrittenAssemblyContext context = new RewrittenAssemblyContext(targetUnwrittenType.Assembly);
+ Type targetWrittenType = context.GetTypeOrThrow(targetUnwrittenType.FullName!);
+
+ object ensuresTestTarget = Activator.CreateInstance(targetWrittenType)!;
+
+ if (exceptionExpected)
+ {
+ Exception? ex = Assert.Catch(() =>
+ {
+ try
+ {
+ CallMethod(targetWrittenType, ensuresTestTarget, methodName, [testNumber]);
+ }
+ catch (TargetInvocationException tie) when (tie.InnerException is not null)
+ {
+ throw tie.InnerException;
+ }
+ });
+ Assert.That(ex, Is.Not.Null);
+ Assert.That(ex!.Message, Contains.Substring("Postcondition not honoured"));
+ }
+ else
+ {
+ Assert.DoesNotThrow(() => CallMethod(targetWrittenType, ensuresTestTarget, methodName, [testNumber]));
+ }
+ }
+
+ private static void CallMethod(Type declaringType, object instance, string methodName, object[] parameters)
+ {
+ MethodInfo method = declaringType.GetMethods().FirstOrDefault(m => m.Name == methodName)
+ ?? throw new InvalidOperationException($"Missing method '{methodName}'.");
+ method.Invoke(instance, parameters);
+ }
+
+ private Type GetTargetTestTypeFor(AttributeFlavour testCase)
+ {
+ if (testCase == AttributeFlavour.Odin)
+ {
+ return typeof(OdinInvariantTestTarget);
+ }
+ if (testCase == AttributeFlavour.BaseClassLibrary)
+ {
+ return typeof(BclInvariantTestTarget);
+ }
+ throw new NotSupportedException(testCase.ToString());
+ }
+
+ private Type GetClassInvariantAttributeTypeFor(AttributeFlavour testCase)
+ {
+ if (testCase == AttributeFlavour.Odin)
+ {
+ return typeof(ClassInvariantMethodAttribute);
+ }
+ if (testCase == AttributeFlavour.BaseClassLibrary)
+ {
+ return typeof(ContractInvariantMethodAttribute);
+ }
+ throw new NotSupportedException(testCase.ToString());
+ }
+}
\ No newline at end of file
diff --git a/DesignContracts/RewriterTests/RewrittenAssemblyContext.cs b/DesignContracts/RewriterTests/RewrittenAssemblyContext.cs
new file mode 100644
index 0000000..ebb26f6
--- /dev/null
+++ b/DesignContracts/RewriterTests/RewrittenAssemblyContext.cs
@@ -0,0 +1,82 @@
+using System.Reflection;
+using System.Runtime.Loader;
+using Odin.DesignContracts.Rewriter;
+
+namespace Tests.Odin.DesignContracts.Rewriter;
+
+///
+/// Encapsulates explicit rewriting of an assembly for testing...
+///
+internal sealed class RewrittenAssemblyContext : IDisposable
+{
+ private readonly AssemblyLoadContext _alc;
+ private readonly string _tempDir;
+
+ public Assembly RewrittenAssembly { get; }
+
+ public RewrittenAssemblyContext(Assembly sourceAssembly)
+ {
+ _tempDir = Path.Combine(Path.GetTempPath(), "rewrite", Guid.NewGuid().ToString("N"));
+ Directory.CreateDirectory(_tempDir);
+
+ string inputPath = Path.Combine(_tempDir, Path.GetFileName(sourceAssembly.Location));
+ File.Copy(sourceAssembly.Location, inputPath, overwrite: true);
+
+ CopyIfExists(Path.ChangeExtension(sourceAssembly.Location, ".pdb"), Path.Combine(_tempDir, Path.GetFileName(Path.ChangeExtension(sourceAssembly.Location, ".pdb"))));
+ CopyIfExists(Path.ChangeExtension(sourceAssembly.Location, ".deps.json"), Path.Combine(_tempDir, Path.GetFileName(Path.ChangeExtension(sourceAssembly.Location, ".deps.json"))));
+
+ string outputPath = Path.Combine(_tempDir, "rewritten.dll");
+ var rewriter = new AssemblyRewriter(inputPath, new ConsoleLoggingAdaptor(), outputPath);
+ rewriter.Rewrite();
+
+ _alc = new TestAssemblyLoadContext(outputPath);
+ RewrittenAssembly = _alc.LoadFromAssemblyPath(outputPath);
+ }
+
+ public Type GetTypeOrThrow(string fullName)
+ => RewrittenAssembly.GetType(fullName, throwOnError: true)!
+ ?? throw new InvalidOperationException($"Type not found in rewritten assembly: {fullName}");
+
+ public void Dispose()
+ {
+ _alc.Unload();
+
+ // Best-effort cleanup. Unload is async-ish; ignore IO failures.
+ try
+ {
+ Directory.Delete(_tempDir, recursive: true);
+ }
+ catch
+ {
+ /* ignore */
+ }
+ }
+
+ private static void CopyIfExists(string from, string to)
+ {
+ if (File.Exists(from))
+ {
+ File.Copy(from, to, overwrite: true);
+ }
+ }
+
+ private sealed class TestAssemblyLoadContext : AssemblyLoadContext
+ {
+ private readonly AssemblyDependencyResolver _resolver;
+
+ public TestAssemblyLoadContext(string mainAssemblyPath)
+ : base(isCollectible: true)
+ {
+ _resolver = new AssemblyDependencyResolver(mainAssemblyPath);
+ }
+
+ protected override Assembly? Load(AssemblyName assemblyName)
+ {
+ string? path = _resolver.ResolveAssemblyToPath(assemblyName);
+ if (path is null)
+ return null;
+
+ return LoadFromAssemblyPath(path);
+ }
+ }
+}
\ No newline at end of file
diff --git a/DesignContracts/RewriterTests/TempDirectory.cs b/DesignContracts/RewriterTests/TempDirectory.cs
new file mode 100644
index 0000000..4000c11
--- /dev/null
+++ b/DesignContracts/RewriterTests/TempDirectory.cs
@@ -0,0 +1,24 @@
+namespace Tests.Odin.DesignContracts.Rewriter;
+
+internal sealed class TempDirectory : IDisposable
+{
+ public string Path { get; }
+
+ public TempDirectory()
+ {
+ Path = System.IO.Path.Combine(System.IO.Path.GetTempPath(), "rewrite", Guid.NewGuid().ToString("N"));
+ Directory.CreateDirectory(Path);
+ }
+
+ public void Dispose()
+ {
+ try
+ {
+ Directory.Delete(Path, recursive: true);
+ }
+ catch
+ {
+ /* ignore */
+ }
+ }
+}
\ No newline at end of file
diff --git a/DesignContracts/RewriterTests/Tests.Odin.DesignContracts.Rewriter.csproj b/DesignContracts/RewriterTests/Tests.Odin.DesignContracts.Rewriter.csproj
new file mode 100644
index 0000000..806819b
--- /dev/null
+++ b/DesignContracts/RewriterTests/Tests.Odin.DesignContracts.Rewriter.csproj
@@ -0,0 +1,33 @@
+
+
+ net8.0;net9.0;net10.0
+ enable
+ true
+ true
+ Tests where the target classes under test have not been weaved in post build
+ by the Design-by-Contract tooling. The Rewriter is explicitly run on a target assembly
+ for each test, and the types under test dynamically loaded.
+ 1591;
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ TestSupport.cs
+
+
+
+
diff --git a/DesignContracts/RewriterTests/TypeRewriterTests.cs b/DesignContracts/RewriterTests/TypeRewriterTests.cs
new file mode 100644
index 0000000..9cffee2
--- /dev/null
+++ b/DesignContracts/RewriterTests/TypeRewriterTests.cs
@@ -0,0 +1,27 @@
+using Mono.Cecil;
+using Moq;
+using NUnit.Framework;
+using Odin.DesignContracts.Rewriter;
+using Targets;
+
+namespace Tests.Odin.DesignContracts.Rewriter;
+
+[TestFixture]
+public sealed class TypeRewriterTests
+{
+ [Test]
+ [TestCase(typeof(OdinInvariantTestTarget), true)]
+ [TestCase(typeof(BclInvariantTestTarget), true)]
+ [TestCase(typeof(NoInvariantTestTarget), false)]
+ public void Invariant_method_is_found(Type type, bool invariantExpected)
+ {
+ CecilAssemblyContext context = CecilAssemblyContext.GetTargetsUntooledAssemblyContext();
+ TypeDefinition? typeDef = context.FindType(type.FullName!);
+ TypeRewriter sut = new TypeRewriter(typeDef!, new Mock().Object);
+
+ Assert.That(sut.HasInvariant, Is.EqualTo(invariantExpected));
+ if (invariantExpected)
+ Assert.That(sut.InvariantMethod, Is.Not.Null);
+ }
+
+}
diff --git a/DesignContracts/TargetsRewritten/TargetsRewritten.csproj b/DesignContracts/TargetsRewritten/TargetsRewritten.csproj
new file mode 100644
index 0000000..a0f5a14
--- /dev/null
+++ b/DesignContracts/TargetsRewritten/TargetsRewritten.csproj
@@ -0,0 +1,41 @@
+
+
+ net8.0;net9.0;net10.0
+ true
+ enable
+ Target classes for the Design Contract rewriter to rewrite
+ at compile time.
+
+ 1591;1573;
+ Targets
+
+ $(DefineConstants);CONTRACTS_FULL
+
+
+
+
+
+
+
+
+
+
+
+ BclInvariantTestTarget.cs
+
+
+ NoInvariantTestTarget.cs
+
+
+ OdinInvariantTestTarget.cs
+
+
+ PostconditionsTestTarget.cs
+
+
+
+
\ No newline at end of file
diff --git a/DesignContracts/TargetsUnrewritten/BclInvariantTestTarget.cs b/DesignContracts/TargetsUnrewritten/BclInvariantTestTarget.cs
new file mode 100644
index 0000000..6267146
--- /dev/null
+++ b/DesignContracts/TargetsUnrewritten/BclInvariantTestTarget.cs
@@ -0,0 +1,62 @@
+using Odin.DesignContracts;
+
+namespace Targets
+{
+ ///
+ /// IMPORTANT: 'CONTRACTS_FULL' needs to be defined as a preprocessor symbol
+ /// if one wishes to use the Bcl System.Diagnostics.Contracts attributes...
+ /// They are conditional.
+ ///
+ public sealed class BclInvariantTestTarget
+ {
+ private int _value;
+
+ public BclInvariantTestTarget(int value)
+ {
+ _value = value;
+ }
+
+ [System.Diagnostics.Contracts.ContractInvariantMethod]
+ public void ObjectInvariant()
+ {
+ Contract.Invariant(_value >= 0, "value must be non-negative");
+ }
+
+ public void Increment()
+ {
+ _value++;
+ }
+
+ public async Task AsyncIncrement()
+ {
+ _value++;
+ return await Task.FromResult(_value);
+ }
+
+ public void MakeInvalid()
+ {
+ _value = -1;
+ }
+
+ public async Task AsyncMakeInvalid()
+ {
+ _value = -1;
+ return await Task.FromResult(_value);
+ }
+
+ [System.Diagnostics.Contracts.Pure]
+ public void PureCommand()
+ {
+
+ }
+
+ [System.Diagnostics.Contracts.Pure]
+ public int PureGetValue() => _value;
+
+ [System.Diagnostics.Contracts.Pure]
+ public int PureProperty => _value;
+
+ public int NonPureProperty => _value;
+
+ }
+}
diff --git a/DesignContracts/TargetsUnrewritten/NoInvariantTestTarget.cs b/DesignContracts/TargetsUnrewritten/NoInvariantTestTarget.cs
new file mode 100644
index 0000000..d6e9f3d
--- /dev/null
+++ b/DesignContracts/TargetsUnrewritten/NoInvariantTestTarget.cs
@@ -0,0 +1,18 @@
+using Odin.DesignContracts;
+
+namespace Targets
+{
+ ///
+ /// The rewriter is expected to inject
+ /// invariant calls at entry/exit of public methods and properties, except where [Pure] is applied.
+ ///
+ public sealed class NoInvariantTestTarget
+ {
+ private int _value;
+
+ public NoInvariantTestTarget(int value)
+ {
+ _value = value;
+ }
+ }
+}
diff --git a/DesignContracts/TargetsUnrewritten/OdinInvariantTestTarget.cs b/DesignContracts/TargetsUnrewritten/OdinInvariantTestTarget.cs
new file mode 100644
index 0000000..81921d3
--- /dev/null
+++ b/DesignContracts/TargetsUnrewritten/OdinInvariantTestTarget.cs
@@ -0,0 +1,80 @@
+using Odin.DesignContracts;
+
+namespace Targets
+{
+ ///
+ /// The rewriter is expected to inject
+ /// invariant calls at entry/exit of public methods and properties, except where [Pure] is applied.
+ ///
+ public sealed class OdinInvariantTestTarget
+ {
+ private int _value;
+
+ public OdinInvariantTestTarget(int value)
+ {
+ _value = value;
+ }
+
+ [ClassInvariantMethod]
+ public void ObjectInvariant()
+ {
+ Contract.Invariant(_value >= 0, "value must be non-negative");
+ }
+
+ public void Increment()
+ {
+ _value++;
+ }
+
+ public async Task AsyncIncrement()
+ {
+ _value++;
+ return await Task.FromResult(_value);
+ }
+
+
+ public void MakeInvalid()
+ {
+ _value = -1;
+ }
+
+ public async Task AsyncMakeInvalid()
+ {
+ _value = -1;
+ return await Task.FromResult(_value);
+ }
+
+ [Pure]
+ public void PureCommand()
+ {
+
+ }
+
+
+ [Pure]
+ public int PureGetValue() => _value;
+
+ [Pure]
+ public int PureProperty => _value;
+
+ public int NonPureProperty => _value;
+
+ public void RequiresYGreaterThan10(int y)
+ {
+ Contract.Requires(y > 10, "y must be greater than 10");
+ Console.WriteLine("Instruction 1");
+ Console.WriteLine("Instruction 2");
+ Console.WriteLine("Instruction 2");
+ }
+
+ public void AssertYGreaterThan10(int y)
+ {
+ Contract.Assert(y > 10, "y must be greater than 10");
+ }
+
+ public void AssumeYGreaterThan10(int y)
+ {
+ Contract.Assume(y > 10, "y must be greater than 10");
+ }
+ }
+}
diff --git a/DesignContracts/TargetsUnrewritten/PostconditionsTestTarget.cs b/DesignContracts/TargetsUnrewritten/PostconditionsTestTarget.cs
new file mode 100644
index 0000000..65dd6ad
--- /dev/null
+++ b/DesignContracts/TargetsUnrewritten/PostconditionsTestTarget.cs
@@ -0,0 +1,129 @@
+
+
+using Odin.DesignContracts;
+
+namespace Targets
+{
+ public sealed class PostconditionsTestTarget
+ {
+ public int Number { get; set; }
+ public string String { get; set; } = "";
+
+ ///
+ /// number = -1 -> failure
+ /// number = 1 -> fine
+ ///
+ ///
+ public void VoidSingleConditionSingleReturn(int number)
+ {
+ Contract.Ensures(Number > 0);
+ Number = number;
+ }
+
+ ///
+ /// 2
+ ///
+ ///
+ public void VoidSingleConditionMultipleReturn(int number)
+ {
+ Contract.Ensures(Number > 0);
+ if (number > 50)
+ {
+ Number = -100;
+ return;
+ }
+ Number = number;
+ }
+
+ ///
+ /// 3
+ ///
+ ///
+ ///
+ public void VoidMultipleConditionsSingleReturn(int number, string aString)
+ {
+ Contract.Ensures(Number > 0);
+ Contract.Ensures(String.Length == 2);
+ Contract.Ensures(Number > 0);
+ Number = number;
+ String = aString;
+ }
+
+ ///
+ /// 4
+ ///
+ ///
+ ///
+ public void VoidMultipleConditionsMultipleReturn(int number, string aString)
+ {
+ Contract.Ensures(Number > 0);
+ Contract.Ensures(String.Length == 2);
+ String = aString;
+ if (number > 100)
+ {
+ Number = -100;
+ return;
+ }
+ Number = number;
+ }
+
+ ///
+ /// 5
+ ///
+ ///
+ public int NotVoidSingleConditionSingleReturn(int number)
+ {
+ Contract.Ensures(Number > 0);
+ Number = number;
+ return Number;
+ }
+
+ ///
+ /// 6
+ ///
+ ///
+ public int NotVoidSingleConditionMultipleReturn(int number)
+ {
+ Contract.Ensures(Number > 0);
+ if (number > 100)
+ {
+ Number = -100;
+ return Number;
+ }
+ Number = number;
+ return Number;
+ }
+
+ ///
+ /// 7
+ ///
+ ///
+ ///
+ public void NotVoidMultipleConditionsSingleReturn(int number, string aString)
+ {
+ Contract.Ensures(Number > 0);
+ Contract.Ensures(String.Length == 2);
+ Contract.Ensures(Number > 0);
+ Number = number;
+ String = aString;
+ }
+
+ ///
+ /// 8
+ ///
+ ///
+ ///
+ public void NotVoidMultipleConditionsMultipleReturn(int number, string aString)
+ {
+ Contract.Ensures(Number > 0);
+ Contract.Ensures(String.Length == 2);
+ String = aString;
+ if (number > 100)
+ {
+ Number = -100;
+ return;
+ }
+ Number = number;
+ }
+ }
+}
diff --git a/DesignContracts/TargetsUnrewritten/TargetsUnrewritten.csproj b/DesignContracts/TargetsUnrewritten/TargetsUnrewritten.csproj
new file mode 100644
index 0000000..d776c3b
--- /dev/null
+++ b/DesignContracts/TargetsUnrewritten/TargetsUnrewritten.csproj
@@ -0,0 +1,15 @@
+
+
+ net8.0;net9.0;net10.0
+ true
+ enable
+ Target classes for the Design Contract rewriter to rewrite
+
+ Targets
+ 1591;1573;
+ $(DefineConstants);CONTRACTS_FULL
+
+
+
+
+
\ No newline at end of file
diff --git a/DesignContracts/Tests/ContractTests.cs b/DesignContracts/Tests/ContractTests.cs
deleted file mode 100644
index 80af0f0..0000000
--- a/DesignContracts/Tests/ContractTests.cs
+++ /dev/null
@@ -1,49 +0,0 @@
-using Odin.DesignContracts;
-using NUnit.Framework;
-
-namespace Tests.Odin.DesignContracts
-{
- [TestFixture]
- public sealed class ContractTests
- {
- [Test]
- [TestCase("not fred.", "(arg != fred)", "Precondition failed: not fred. [Condition: (arg != fred)]")]
- [TestCase("not fred.", " ", "Precondition failed: not fred.")]
- [TestCase("not fred.", null, "Precondition failed: not fred.")]
- [TestCase("not fred.", "", "Precondition failed: not fred.")]
- [TestCase("", "", "Precondition failed.")]
- [TestCase("", null, "Precondition failed.")]
- [TestCase(" ", null, "Precondition failed.")]
- [TestCase(null, null, "Precondition failed.")]
- [TestCase(null, "", "Precondition failed.")]
- [TestCase(null, " ", "Precondition failed.")]
- [TestCase(null, "(arg==0)", "Precondition failed: (arg==0)")]
- public void Requires_throws_exception_with_correct_message_on_precondition_failure(string conditionDescription, string? conditionText, string expectedExceptionMessage)
- {
- ContractException? ex = Assert.Throws(() => Precondition.Requires(false, conditionDescription,conditionText));
- Assert.That(ex, Is.Not.Null);
- Assert.That(ex!.Message, Is.EqualTo(expectedExceptionMessage), "Exception message is incorrect");
- }
-
- [Test]
- public void Requires_does_not_throw_exception_on_precondition_success()
- {
- Assert.DoesNotThrow(() => Precondition.Requires(true, "Message"), "Precondition success must not throw an Exception");
- }
- }
-
- [TestFixture(typeof(ArgumentNullException))]
- [TestFixture(typeof(ArgumentException))]
- [TestFixture(typeof(DivideByZeroException))]
- public sealed class ContractRequiresGenericTests where TException : Exception
- {
- [Test]
- public void Requires_throws_specific_exception_on_precondition_failure()
- {
- TException? ex = Assert.Throws(() => Precondition.Requires(false, "msg"));
-
- Assert.That(ex, Is.Not.Null);
- Assert.That(ex, Is.InstanceOf());
- }
- }
-}
\ No newline at end of file
diff --git a/DesignContracts/Tooling/Odin.DesignContracts.Tooling.csproj b/DesignContracts/Tooling/Odin.DesignContracts.Tooling.csproj
new file mode 100644
index 0000000..781e3e0
--- /dev/null
+++ b/DesignContracts/Tooling/Odin.DesignContracts.Tooling.csproj
@@ -0,0 +1,64 @@
+
+
+ net8.0;net9.0;net10.0
+ true
+ enable
+
+ true
+ Odin.DesignContracts.Tooling
+ Design-by-Contract tooling for Odin.DesignContracts: Analyzers + IL rewriter integration.
+ icon.png
+ 1591;1573;
+ true
+
+
+
+
+
+
+
+
+
+ $(MSBuildProjectDirectory)/../Rewriter/bin/$(Configuration)/$(TargetFramework)/
+ $(MSBuildProjectDirectory)/tools/$(TargetFramework)/any/
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ <_Tfms ToLower="true" Include="$(TargetFrameworks)"/>
+ <_PackageFiles Include="../Rewriter/bin/$(Configuration)/%(_Tfms.Identity)/Odin.DesignContracts.Rewriter.dll">
+ tools/%(_Tfms.Identity)/any/
+
+ <_PackageFiles Include="../Rewriter/bin/$(Configuration)/%(_Tfms.Identity)/Odin.DesignContracts.Rewriter.runtimeconfig.json">
+ tools/%(_Tfms.Identity)/any/
+
+ <_PackageFiles Include="../Rewriter/bin/$(Configuration)/%(_Tfms.Identity)/Odin.DesignContracts.Rewriter.deps.json">
+ tools/%(_Tfms.Identity)/any/
+
+
+
+
+
+
+
+
+
diff --git a/DesignContracts/Tooling/buildTransitive/Odin.DesignContracts.Tooling.targets b/DesignContracts/Tooling/buildTransitive/Odin.DesignContracts.Tooling.targets
new file mode 100644
index 0000000..809602b
--- /dev/null
+++ b/DesignContracts/Tooling/buildTransitive/Odin.DesignContracts.Tooling.targets
@@ -0,0 +1,34 @@
+
+
+
+
+ true
+
+
+ true
+
+
+
+
+
+
+
+
+ $(MSBuildProjectDirectory)/$(IntermediateOutputPath)$(TargetFileName)
+
+
+
+
+
+
+
+
+
+
+
diff --git a/Email/Core/Attachment.cs b/Email/Core/Attachment.cs
index 04162e5..1ed5df1 100644
--- a/Email/Core/Attachment.cs
+++ b/Email/Core/Attachment.cs
@@ -17,9 +17,9 @@ public sealed record Attachment
///
public Attachment(string fileName, Stream data, string contentType)
{
- Precondition.Requires(!string.IsNullOrWhiteSpace(fileName));
- Precondition.Requires(!string.IsNullOrWhiteSpace(contentType));
- Precondition.RequiresNotNull(data);
+ Contract.Requires(!string.IsNullOrWhiteSpace(fileName));
+ Contract.Requires(!string.IsNullOrWhiteSpace(contentType));
+ Contract.RequiresNotNull(data);
FileName = fileName;
Data = data;
ContentType = contentType;
diff --git a/Email/Core/DependencyInjectionExtensions.cs b/Email/Core/DependencyInjectionExtensions.cs
index c95ad4d..035ca4f 100644
--- a/Email/Core/DependencyInjectionExtensions.cs
+++ b/Email/Core/DependencyInjectionExtensions.cs
@@ -41,7 +41,7 @@ public static void AddOdinEmailSending(
public static void AddOdinEmailSending(
this IServiceCollection serviceCollection, IConfigurationSection configurationSection)
{
- Precondition.RequiresNotNull(configurationSection);
+ Contract.RequiresNotNull(configurationSection);
EmailSendingOptions emailOptions = new EmailSendingOptions();
configurationSection.Bind(emailOptions);
diff --git a/Email/Core/EmailAddress.cs b/Email/Core/EmailAddress.cs
index a156070..041707a 100644
--- a/Email/Core/EmailAddress.cs
+++ b/Email/Core/EmailAddress.cs
@@ -24,7 +24,7 @@ public sealed class EmailAddress
///
public EmailAddress(string emailAddress, string? displayName = null)
{
- Precondition.Requires(!string.IsNullOrWhiteSpace(emailAddress), $"{nameof(emailAddress)} is required");
+ Contract.Requires(!string.IsNullOrWhiteSpace(emailAddress), $"{nameof(emailAddress)} is required");
if (string.IsNullOrWhiteSpace(displayName))
{
DisplayName = null;
diff --git a/Email/Core/EmailMessage.cs b/Email/Core/EmailMessage.cs
index 1ded116..3920d3e 100644
--- a/Email/Core/EmailMessage.cs
+++ b/Email/Core/EmailMessage.cs
@@ -29,9 +29,9 @@ public EmailMessage()
public EmailMessage(string toEmailAddress, string fromEmailAddress, string? subject, string? body,
bool isHtml = false)
{
- Precondition.Requires(!string.IsNullOrWhiteSpace(toEmailAddress),
+ Contract.Requires(!string.IsNullOrWhiteSpace(toEmailAddress),
$"{nameof(toEmailAddress)} is required");
- Precondition.Requires(!string.IsNullOrWhiteSpace(fromEmailAddress),
+ Contract.Requires(!string.IsNullOrWhiteSpace(fromEmailAddress),
$"{nameof(fromEmailAddress)} is required");
if (string.IsNullOrWhiteSpace(subject))
{
@@ -207,7 +207,7 @@ public Dictionary Headers
///
public void Attach(Attachment attachment)
{
- Precondition.RequiresNotNull(attachment);
+ Contract.RequiresNotNull(attachment);
Attachments.Add(attachment);
}
}
diff --git a/Email/Core/EmailSendingOptions.cs b/Email/Core/EmailSendingOptions.cs
index 6b5840a..20afb4c 100644
--- a/Email/Core/EmailSendingOptions.cs
+++ b/Email/Core/EmailSendingOptions.cs
@@ -52,7 +52,7 @@ public string Provider
get => _provider;
init
{
- Precondition.Requires(!string.IsNullOrWhiteSpace(value));
+ Contract.Requires(!string.IsNullOrWhiteSpace(value));
// Ensure MailgunEmailSender is changed to Mailgun for backwards compatibility
_provider = value.Replace("EmailSender", "", StringComparison.OrdinalIgnoreCase);
}
diff --git a/Email/Mailgun/MailgunEmailSender.cs b/Email/Mailgun/MailgunEmailSender.cs
index 62c474b..765b655 100644
--- a/Email/Mailgun/MailgunEmailSender.cs
+++ b/Email/Mailgun/MailgunEmailSender.cs
@@ -42,9 +42,9 @@ public sealed class MailgunEmailSender : IEmailSender
public MailgunEmailSender(MailgunOptions mailgunSettings,
EmailSendingOptions emailSettings, ILoggerWrapper logger)
{
- Precondition.RequiresNotNull(mailgunSettings);
- Precondition.RequiresNotNull(emailSettings);
- Precondition.RequiresNotNull(logger);
+ Contract.RequiresNotNull(mailgunSettings);
+ Contract.RequiresNotNull(emailSettings);
+ Contract.RequiresNotNull(logger);
_mailgunSettings = mailgunSettings;
_emailSettings = emailSettings;
_logger = logger;
@@ -59,7 +59,7 @@ public MailgunEmailSender(MailgunOptions mailgunSettings,
endPoint += "/";
}
- Precondition.Requires(!string.IsNullOrWhiteSpace(_mailgunSettings.Domain), "Domain missing in MailgunOptions");
+ Contract.Requires(!string.IsNullOrWhiteSpace(_mailgunSettings.Domain), "Domain missing in MailgunOptions");
string subPath = $"{_mailgunSettings.Domain}/messages";
// Leading slash will replace the /v3
if (subPath[0] == '/')
@@ -68,7 +68,7 @@ public MailgunEmailSender(MailgunOptions mailgunSettings,
}
_httpClient.BaseAddress = new Uri(new Uri(endPoint), subPath);
- Precondition.Requires(!string.IsNullOrWhiteSpace(_mailgunSettings.ApiKey), "ApiKey missing in MailgunOptions");
+ Contract.Requires(!string.IsNullOrWhiteSpace(_mailgunSettings.ApiKey), "ApiKey missing in MailgunOptions");
byte[] byteArray = Encoding.ASCII.GetBytes($"api:{_mailgunSettings.ApiKey}");
_httpClient.DefaultRequestHeaders.Authorization = new AuthenticationHeaderValue(
@@ -85,9 +85,9 @@ private static string EncodeAsHtml(string input)
private static ByteArrayContent ToByteArrayContent(Stream stream)
{
- Precondition.RequiresNotNull(stream);
- Precondition.Requires(stream.CanRead, "Stream.CanRead must be true");
- Precondition.Requires(stream.CanSeek, "Stream.CanSeek must be true");
+ Contract.RequiresNotNull(stream);
+ Contract.Requires(stream.CanRead, "Stream.CanRead must be true");
+ Contract.Requires(stream.CanSeek, "Stream.CanSeek must be true");
try
{
@@ -112,9 +112,9 @@ private static ByteArrayContent ToByteArrayContent(Stream stream)
///
public async Task> SendEmail(IEmailMessage email)
{
- Precondition.RequiresNotNull(email);
- Precondition.Requires(email.To.Any(), "Mailgun requires one or more to addresses.");
- Precondition.Requires(!string.IsNullOrWhiteSpace(email.Subject), "Mailgun requires an email subject");
+ Contract.RequiresNotNull(email);
+ Contract.Requires(email.To.Any(), "Mailgun requires one or more to addresses.");
+ Contract.Requires(!string.IsNullOrWhiteSpace(email.Subject), "Mailgun requires an email subject");
try
{
diff --git a/Email/Mailgun/MailgunServiceInjector.cs b/Email/Mailgun/MailgunServiceInjector.cs
index 11e4977..4477c45 100644
--- a/Email/Mailgun/MailgunServiceInjector.cs
+++ b/Email/Mailgun/MailgunServiceInjector.cs
@@ -15,7 +15,7 @@ public class MailgunServiceInjector : IEmailSenderServiceInjector
public void TryAddEmailSender(IServiceCollection serviceCollection,
IConfigurationSection emailConfigurationSection)
{
- Precondition.RequiresNotNull(emailConfigurationSection);
+ Contract.RequiresNotNull(emailConfigurationSection);
MailgunOptions mailGunSenderSettings = new MailgunOptions();
emailConfigurationSection.Bind(MailgunOptions.MailgunName,
diff --git a/Email/Office365/Office365EmailSender.cs b/Email/Office365/Office365EmailSender.cs
index 2028f92..084c58e 100644
--- a/Email/Office365/Office365EmailSender.cs
+++ b/Email/Office365/Office365EmailSender.cs
@@ -3,7 +3,6 @@
using Microsoft.Graph;
using Microsoft.Graph.Models;
using Microsoft.Graph.Users.Item.SendMail;
-using Odin.DesignContracts;
using Odin.Logging;
using Odin.System;
using Contract = Odin.DesignContracts.Contract;
@@ -28,9 +27,9 @@ public class Office365EmailSender : IEmailSender
/// Microsoft UserId
public Office365EmailSender(Office365Options office365Options, EmailSendingOptions emailSettings , ILoggerWrapper logger)
{
- Precondition.RequiresNotNull(office365Options);
- Precondition.RequiresNotNull(emailSettings);
- Precondition.RequiresNotNull(logger);
+ Contract.RequiresNotNull(office365Options);
+ Contract.RequiresNotNull(emailSettings);
+ Contract.RequiresNotNull(logger);
_emailSettings = emailSettings;
_logger = logger;
@@ -60,7 +59,7 @@ public async Task> SendEmail(IEmailMessage email)
{
if (email.From is null)
{
- Precondition.Requires(!string.IsNullOrWhiteSpace(_emailSettings.DefaultFromAddress), "Cannot fall back to the default from address, since it is missing.");
+ Contract.Requires(!string.IsNullOrWhiteSpace(_emailSettings.DefaultFromAddress), "Cannot fall back to the default from address, since it is missing.");
email.From = new EmailAddress(_emailSettings.DefaultFromAddress!, _emailSettings.DefaultFromName);
}
email.Subject = string.Concat(_emailSettings.SubjectPrefix, email.Subject,
diff --git a/Email/Office365/Office365ServiceInjector.cs b/Email/Office365/Office365ServiceInjector.cs
index 99fe8d3..6462ae8 100644
--- a/Email/Office365/Office365ServiceInjector.cs
+++ b/Email/Office365/Office365ServiceInjector.cs
@@ -11,7 +11,7 @@ public class Office365ServiceInjector : IEmailSenderServiceInjector
///
public void TryAddEmailSender(IServiceCollection serviceCollection, IConfigurationSection emailConfigurationSection)
{
- Precondition.RequiresNotNull(emailConfigurationSection);
+ Contract.RequiresNotNull(emailConfigurationSection);
EmailSendingOptions emailOptions = new();
emailConfigurationSection.Bind(emailOptions);
diff --git a/Email/Tests/EmailTestConfiguration.cs b/Email/Tests/EmailTestConfiguration.cs
index 90aca14..dcc2c2b 100644
--- a/Email/Tests/EmailTestConfiguration.cs
+++ b/Email/Tests/EmailTestConfiguration.cs
@@ -7,13 +7,13 @@ public static class EmailTestConfiguration
{
public static string GetTestEmailAddressFromConfig(IConfiguration config)
{
- Precondition.RequiresNotNull(config);
+ Contract.RequiresNotNull(config);
return config["Email-TestToAddress"]!;
}
public static string GetTestFromNameFromConfig(IConfiguration config)
{
- Precondition.RequiresNotNull(config);
+ Contract.RequiresNotNull(config);
return config["Email-TestFromName"]!;
}
}
\ No newline at end of file
diff --git a/Email/Tests/Mailgun/MailgunEmailSenderTestBuilder.cs b/Email/Tests/Mailgun/MailgunEmailSenderTestBuilder.cs
index 9859ab0..c46d27d 100644
--- a/Email/Tests/Mailgun/MailgunEmailSenderTestBuilder.cs
+++ b/Email/Tests/Mailgun/MailgunEmailSenderTestBuilder.cs
@@ -44,7 +44,7 @@ public MailgunEmailSenderTestBuilder EnsureNullDependenciesAreMocked()
public MailgunEmailSenderTestBuilder WithEmailSendingOptionsFromTestConfiguration(IConfiguration configuration)
{
- Precondition.RequiresNotNull(configuration);
+ Contract.RequiresNotNull(configuration);
string testerEmail = EmailTestConfiguration.GetTestEmailAddressFromConfig(configuration);
string testerName = EmailTestConfiguration.GetTestFromNameFromConfig(configuration);
EmailSendingOptions = new EmailSendingOptions()
@@ -67,7 +67,7 @@ public MailgunEmailSenderTestBuilder WithMailgunOptionsFromTestConfiguration(ICo
public static MailgunOptions GetMailgunOptionsFromConfig(IConfiguration config)
{
- Precondition.RequiresNotNull(config);
+ Contract.RequiresNotNull(config);
IConfigurationSection section = config.GetSection("Email-MailgunOptions");
MailgunOptions options = new MailgunOptions();
section.Bind(options);
diff --git a/Email/Tests/Office365/Office365EmailSenderTestBuilder.cs b/Email/Tests/Office365/Office365EmailSenderTestBuilder.cs
index 1ce3ace..f3e1407 100644
--- a/Email/Tests/Office365/Office365EmailSenderTestBuilder.cs
+++ b/Email/Tests/Office365/Office365EmailSenderTestBuilder.cs
@@ -43,7 +43,7 @@ public Office365EmailSenderTestBuilder EnsureNullDependenciesAreMocked()
public Office365EmailSenderTestBuilder WithEmailSendingOptionsFromTestConfiguration(IConfiguration configuration)
{
- Precondition.RequiresNotNull(configuration);
+ Contract.RequiresNotNull(configuration);
string testerEmail = EmailTestConfiguration.GetTestEmailAddressFromConfig(configuration);
string testerName = EmailTestConfiguration.GetTestFromNameFromConfig(configuration);
EmailSendingOptions = new EmailSendingOptions()
@@ -66,7 +66,7 @@ public Office365EmailSenderTestBuilder WithOffice365OptionsFromTestConfiguration
public static Office365Options GetOffice365OptionsFromConfig(IConfiguration config)
{
- Precondition.RequiresNotNull(config);
+ Contract.RequiresNotNull(config);
IConfigurationSection section = config.GetSection("Email-Office365");
Office365Options options = new Office365Options();
section.Bind(options);
diff --git a/Odin.sln b/Odin.sln
index 108f5ae..9b46bc4 100644
--- a/Odin.sln
+++ b/Odin.sln
@@ -90,7 +90,7 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Tests.Odin.Templating", "Te
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Tests.Odin.Utility", "Utility\Tests\Tests.Odin.Utility.csproj", "{52AF2C63-2247-42FD-B3DD-4AD2AFCE0C6D}"
EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Tests.Odin.DesignContracts", "DesignContracts\Tests\Tests.Odin.DesignContracts.csproj", "{177EDB52-3174-4037-80DD-235222F9817B}"
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Tests.Odin.DesignContracts", "DesignContracts\CoreTests\Tests.Odin.DesignContracts.csproj", "{177EDB52-3174-4037-80DD-235222F9817B}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Tests.Odin.Messaging", "Messaging\Tests\Tests.Odin.Messaging.csproj", "{690312C5-1948-4530-832D-6332625D4E9C}"
EndProject
@@ -98,6 +98,16 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Tests.Odin.System", "System
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Odin.DesignContracts.Analyzers", "DesignContracts\Analyzers\Odin.DesignContracts.Analyzers.csproj", "{12C40512-CA83-4209-9318-6CBCABF8C798}"
EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Odin.DesignContracts.Rewriter", "DesignContracts\Rewriter\Odin.DesignContracts.Rewriter.csproj", "{60A2A141-EAC8-4EAB-850D-AF534ABFE98C}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Odin.DesignContracts.Tooling", "DesignContracts\Tooling\Odin.DesignContracts.Tooling.csproj", "{B25A8EAA-5FD6-4A47-96A1-2C7108FC4576}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Tests.Odin.DesignContracts.Rewriter", "DesignContracts\RewriterTests\Tests.Odin.DesignContracts.Rewriter.csproj", "{320907F6-F4BA-4A1D-AC23-145A5AD06C14}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "TargetsUnrewritten", "DesignContracts\TargetsUnrewritten\TargetsUnrewritten.csproj", "{7BC62DE2-D0F7-4CD9-83D0-C47BE760F33D}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "TargetsRewritten", "DesignContracts\TargetsRewritten\TargetsRewritten.csproj", "{8138E8B4-E90D-45A3-BEB0-31F048948A91}"
+EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
Debug|Any CPU = Debug|Any CPU
@@ -224,6 +234,26 @@ Global
{12C40512-CA83-4209-9318-6CBCABF8C798}.Debug|Any CPU.Build.0 = Debug|Any CPU
{12C40512-CA83-4209-9318-6CBCABF8C798}.Release|Any CPU.ActiveCfg = Release|Any CPU
{12C40512-CA83-4209-9318-6CBCABF8C798}.Release|Any CPU.Build.0 = Release|Any CPU
+ {60A2A141-EAC8-4EAB-850D-AF534ABFE98C}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {60A2A141-EAC8-4EAB-850D-AF534ABFE98C}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {60A2A141-EAC8-4EAB-850D-AF534ABFE98C}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {60A2A141-EAC8-4EAB-850D-AF534ABFE98C}.Release|Any CPU.Build.0 = Release|Any CPU
+ {B25A8EAA-5FD6-4A47-96A1-2C7108FC4576}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {B25A8EAA-5FD6-4A47-96A1-2C7108FC4576}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {B25A8EAA-5FD6-4A47-96A1-2C7108FC4576}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {B25A8EAA-5FD6-4A47-96A1-2C7108FC4576}.Release|Any CPU.Build.0 = Release|Any CPU
+ {320907F6-F4BA-4A1D-AC23-145A5AD06C14}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {320907F6-F4BA-4A1D-AC23-145A5AD06C14}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {320907F6-F4BA-4A1D-AC23-145A5AD06C14}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {320907F6-F4BA-4A1D-AC23-145A5AD06C14}.Release|Any CPU.Build.0 = Release|Any CPU
+ {7BC62DE2-D0F7-4CD9-83D0-C47BE760F33D}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {7BC62DE2-D0F7-4CD9-83D0-C47BE760F33D}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {7BC62DE2-D0F7-4CD9-83D0-C47BE760F33D}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {7BC62DE2-D0F7-4CD9-83D0-C47BE760F33D}.Release|Any CPU.Build.0 = Release|Any CPU
+ {8138E8B4-E90D-45A3-BEB0-31F048948A91}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {8138E8B4-E90D-45A3-BEB0-31F048948A91}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {8138E8B4-E90D-45A3-BEB0-31F048948A91}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {8138E8B4-E90D-45A3-BEB0-31F048948A91}.Release|Any CPU.Build.0 = Release|Any CPU
EndGlobalSection
GlobalSection(NestedProjects) = preSolution
{CE323D9C-635B-EFD3-5B3F-7CE371D8A86A} = {BF440C74-E223-3CBF-8FA7-83F7D164F7C3}
@@ -244,6 +274,7 @@ Global
{2B952295-4016-E1DA-8A6A-A0084F2049DF} = {9E3E1A13-9A74-4895-98A9-D96F4E0ED4B7}
{957731CC-1C44-4D0C-58F8-9B67862EF843} = {6D4C8AB9-F597-49BD-91D3-081FA1845584}
{21717156-66D0-2EF7-4728-A1BDEC5395F1} = {4140B1D5-6C97-4F68-8DEA-C0D139BA9FBC}
+ {E450FC74-0DBE-320A-FE7A-87255CB4DFAB} = {3610DE71-0841-E98B-B5EB-0B69D343489C}
{36463D1F-7E51-41B8-B6EA-5E3B833DB479} = {73BA62BB-2B41-2DC4-C714-51B3D4C2A215}
{13D2E2D9-7E61-4AED-83C6-71D01D6E3BFD} = {73BA62BB-2B41-2DC4-C714-51B3D4C2A215}
{B091589D-960C-40F6-822F-522D099828E6} = {BF440C74-E223-3CBF-8FA7-83F7D164F7C3}
@@ -255,6 +286,11 @@ Global
{690312C5-1948-4530-832D-6332625D4E9C} = {4140B1D5-6C97-4F68-8DEA-C0D139BA9FBC}
{957966BC-FE0E-4206-BDD8-F04591AB836E} = {73BA62BB-2B41-2DC4-C714-51B3D4C2A215}
{12C40512-CA83-4209-9318-6CBCABF8C798} = {9E3E1A13-9A74-4895-98A9-D96F4E0ED4B7}
+ {60A2A141-EAC8-4EAB-850D-AF534ABFE98C} = {9E3E1A13-9A74-4895-98A9-D96F4E0ED4B7}
+ {B25A8EAA-5FD6-4A47-96A1-2C7108FC4576} = {9E3E1A13-9A74-4895-98A9-D96F4E0ED4B7}
{E450FC74-0DBE-320A-FE7A-87255CB4DFAB} = {73BA62BB-2B41-2DC4-C714-51B3D4C2A215}
+ {320907F6-F4BA-4A1D-AC23-145A5AD06C14} = {9E3E1A13-9A74-4895-98A9-D96F4E0ED4B7}
+ {7BC62DE2-D0F7-4CD9-83D0-C47BE760F33D} = {9E3E1A13-9A74-4895-98A9-D96F4E0ED4B7}
+ {8138E8B4-E90D-45A3-BEB0-31F048948A91} = {9E3E1A13-9A74-4895-98A9-D96F4E0ED4B7}
EndGlobalSection
EndGlobal
diff --git a/RemoteFiles/Abstractions/RemoteFileInfo.cs b/RemoteFiles/Abstractions/RemoteFileInfo.cs
index e84c4b3..6e96a31 100644
--- a/RemoteFiles/Abstractions/RemoteFileInfo.cs
+++ b/RemoteFiles/Abstractions/RemoteFileInfo.cs
@@ -15,8 +15,8 @@ public sealed class RemoteFileInfo : IRemoteFileInfo
///
public RemoteFileInfo(string fullName, string name, DateTime lastWriteTimeUtc)
{
- Precondition.Requires(!string.IsNullOrWhiteSpace(name), nameof(name));
- Precondition.Requires(!string.IsNullOrWhiteSpace(fullName), nameof(fullName));
+ Contract.Requires(!string.IsNullOrWhiteSpace(name), nameof(name));
+ Contract.Requires(!string.IsNullOrWhiteSpace(fullName), nameof(fullName));
FullName = fullName;
Name = name;
// Use overload for DateTimeOffset set from DateTime
diff --git a/RemoteFiles/Core/ConnectionSettingsHelper.cs b/RemoteFiles/Core/ConnectionSettingsHelper.cs
index a0f56e3..353eb0f 100644
--- a/RemoteFiles/Core/ConnectionSettingsHelper.cs
+++ b/RemoteFiles/Core/ConnectionSettingsHelper.cs
@@ -27,7 +27,7 @@ public static class ConnectionSettingsHelper
///
public static Dictionary ParseConnectionString(string connectionString, char delimiter)
{
- Precondition.Requires(!string.IsNullOrEmpty(connectionString), "connectionString cannot be null.");
+ Contract.Requires(!string.IsNullOrEmpty(connectionString), "connectionString cannot be null.");
Dictionary result = new Dictionary();
string[] keyValuePairs = connectionString.Trim(delimiter).Split(delimiter)
diff --git a/RemoteFiles/Core/DependencyInjectionExtensions.cs b/RemoteFiles/Core/DependencyInjectionExtensions.cs
index 3ea191d..5e6ae2a 100644
--- a/RemoteFiles/Core/DependencyInjectionExtensions.cs
+++ b/RemoteFiles/Core/DependencyInjectionExtensions.cs
@@ -33,7 +33,7 @@ public static IServiceCollection AddRemoteFiles(this IServiceCollection services
public static IServiceCollection AddRemoteFiles(this IServiceCollection services,
IConfigurationSection configurationSection)
{
- Precondition.Requires(configurationSection!=null!, "Configuration Section for RemoteFiles cannot be null.");
+ Contract.Requires(configurationSection!=null!, "Configuration Section for RemoteFiles cannot be null.");
if (!configurationSection.Exists())
throw new ApplicationException(
diff --git a/RemoteFiles/Core/RemoteFileSessionFactory.cs b/RemoteFiles/Core/RemoteFileSessionFactory.cs
index a5fe96f..d0e74af 100644
--- a/RemoteFiles/Core/RemoteFileSessionFactory.cs
+++ b/RemoteFiles/Core/RemoteFileSessionFactory.cs
@@ -17,8 +17,8 @@ public class RemoteFileSessionFactory : IRemoteFileSessionFactory
///
public RemoteFileSessionFactory(RemoteFilesOptions remoteFilesOptions)
{
- Precondition.Requires(remoteFilesOptions != null, "remoteFileConfiguration cannot be null");
- Precondition.Requires(remoteFilesOptions.ConnectionStrings != null, "remoteFileConfiguration connection strings cannot null");
+ Contract.Requires(remoteFilesOptions != null, "remoteFileConfiguration cannot be null");
+ Contract.Requires(remoteFilesOptions.ConnectionStrings != null, "remoteFileConfiguration connection strings cannot null");
_fileSourceConnections = remoteFilesOptions.ConnectionStrings.ToDictionary(
kv => kv.Key,
@@ -37,7 +37,7 @@ public RemoteFileSessionFactory(RemoteFilesOptions remoteFilesOptions)
///
public ResultValue CreateRemoteFileSession(string connectionName)
{
- Precondition.Requires(!string.IsNullOrEmpty(connectionName), "connectionName cannot be null");
+ Contract.Requires(!string.IsNullOrEmpty(connectionName), "connectionName cannot be null");
if (!_fileSourceConnections.ContainsKey(connectionName))
return ResultValue.Failure($"Connection name not supported or configured: {connectionName}");
diff --git a/RemoteFiles/SFTP/SftpRemoteFileSession.cs b/RemoteFiles/SFTP/SftpRemoteFileSession.cs
index 3596bb4..226e36f 100644
--- a/RemoteFiles/SFTP/SftpRemoteFileSession.cs
+++ b/RemoteFiles/SFTP/SftpRemoteFileSession.cs
@@ -21,7 +21,7 @@ public sealed class SftpRemoteFileSession : IRemoteFileSession
///
public SftpRemoteFileSession(SftpConnectionSettings connectionInfo)
{
- Precondition.Requires(connectionInfo!=null!);
+ Contract.Requires(connectionInfo!=null!);
_connectionInfo = connectionInfo!;
}
@@ -98,8 +98,8 @@ public void Disconnect()
///
public void UploadFile(string textFileContents, string fileName)
{
- Precondition.Requires(textFileContents != null, nameof(textFileContents));
- Precondition.Requires(!string.IsNullOrWhiteSpace(fileName), nameof(fileName));
+ Contract.Requires(textFileContents != null, nameof(textFileContents));
+ Contract.Requires(!string.IsNullOrWhiteSpace(fileName), nameof(fileName));
EnsureConnected();
MemoryStream stream = new MemoryStream(Encoding.ASCII.GetBytes(textFileContents));
@@ -115,7 +115,7 @@ public void UploadFile(string textFileContents, string fileName)
///
public void DownloadFile(string fileName, in Stream output)
{
- Precondition.Requires(!string.IsNullOrWhiteSpace(fileName), nameof(fileName));
+ Contract.Requires(!string.IsNullOrWhiteSpace(fileName), nameof(fileName));
EnsureConnected();
_client!.BufferSize = 4096;
@@ -148,7 +148,7 @@ public string DownloadTextFile(string fileName)
///
public void ChangeDirectory(string path)
{
- Precondition.Requires(!string.IsNullOrWhiteSpace(path), nameof(path));
+ Contract.Requires(!string.IsNullOrWhiteSpace(path), nameof(path));
EnsureConnected();
_client.ChangeDirectory(path);
}
@@ -159,7 +159,7 @@ public void ChangeDirectory(string path)
///
public void CreateDirectory(string path)
{
- Precondition.Requires(!string.IsNullOrWhiteSpace(path), nameof(path));
+ Contract.Requires(!string.IsNullOrWhiteSpace(path), nameof(path));
EnsureConnected();
_client!.CreateDirectory(path);
}
@@ -170,7 +170,7 @@ public void CreateDirectory(string path)
///
public void Delete(string filePath)
{
- Precondition.Requires(!string.IsNullOrWhiteSpace(filePath), nameof(filePath));
+ Contract.Requires(!string.IsNullOrWhiteSpace(filePath), nameof(filePath));
EnsureConnected();
_client!.DeleteFile(filePath);
}
@@ -183,8 +183,8 @@ public void Delete(string filePath)
///
public IEnumerable GetFiles(string path, string? searchPattern = null)
{
- Precondition.Requires(!string.IsNullOrWhiteSpace(path), nameof(path));
- Precondition.Requires(!(path!.Contains('*') || path.Contains('?')));
+ Contract.Requires(!string.IsNullOrWhiteSpace(path), nameof(path));
+ Contract.Requires(!(path!.Contains('*') || path.Contains('?')));
EnsureConnected();
//return results
IEnumerable files = _client.ListDirectory(path);
@@ -210,7 +210,7 @@ public IEnumerable GetFiles(string path, string? searchPattern
///
public bool Exists(string path, int? timeoutInSeconds = null)
{
- Precondition.Requires(!string.IsNullOrWhiteSpace(path), nameof(path));
+ Contract.Requires(!string.IsNullOrWhiteSpace(path), nameof(path));
EnsureConnected(timeoutInSeconds);
return _client.Exists(path);
}
diff --git a/System/Activator2/Activator2.cs b/System/Activator2/Activator2.cs
index b99780a..05882b2 100644
--- a/System/Activator2/Activator2.cs
+++ b/System/Activator2/Activator2.cs
@@ -16,8 +16,8 @@ public static class Activator2
///
public static ResultValue TryCreate(string typeName, string assemblyName) where T : class
{
- Precondition.Requires(!string.IsNullOrWhiteSpace(typeName));
- Precondition.Requires(!string.IsNullOrWhiteSpace(assemblyName));
+ Contract.Requires(!string.IsNullOrWhiteSpace(typeName));
+ Contract.Requires(!string.IsNullOrWhiteSpace(assemblyName));
ObjectHandle? handle;
try
{
@@ -50,7 +50,7 @@ private static ResultValue CreateInstanceFailure(string typeName, string a
///
public static ResultValue TryCreate(Type typeToCreate) where T : class
{
- Precondition.Requires(typeToCreate!=null!);
+ Contract.Requires(typeToCreate!=null!);
try
{
object? obj = Activator.CreateInstance(typeToCreate);
diff --git a/System/Tests/ResultOfTMessageTests.cs b/System/Tests/ResultOfTMessageTests.cs
index f280d83..989945e 100644
--- a/System/Tests/ResultOfTMessageTests.cs
+++ b/System/Tests/ResultOfTMessageTests.cs
@@ -1,5 +1,4 @@
-using System.Text.Json;
-using NUnit.Framework;
+using NUnit.Framework;
using Odin.System;
namespace Tests.Odin.System
diff --git a/TestsOnly.sln b/TestsOnly.sln
index 5e54937..fd54c0d 100644
--- a/TestsOnly.sln
+++ b/TestsOnly.sln
@@ -10,8 +10,6 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Tests.Odin.Templating", "Te
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Tests.Odin.Utility", "Utility\Tests\Tests.Odin.Utility.csproj", "{52AF2C63-2247-42FD-B3DD-4AD2AFCE0C6D}"
EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Tests.Odin.DesignContracts", "DesignContracts\Tests\Tests.Odin.DesignContracts.csproj", "{177EDB52-3174-4037-80DD-235222F9817B}"
-EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Tests.Odin.Messaging", "Messaging\Tests\Tests.Odin.Messaging.csproj", "{690312C5-1948-4530-832D-6332625D4E9C}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Tests.Odin.System", "System\Tests\Tests.Odin.System.csproj", "{957966BC-FE0E-4206-BDD8-F04591AB836E}"
@@ -23,8 +21,6 @@ Global
GlobalSection(ProjectConfigurationPlatforms) = postSolution
{B091589D-960C-40F6-822F-522D099828E6}.Release|Any CPU.ActiveCfg = Release|Any CPU
{B091589D-960C-40F6-822F-522D099828E6}.Release|Any CPU.Build.0 = Release|Any CPU
- {177EDB52-3174-4037-80DD-235222F9817B}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {177EDB52-3174-4037-80DD-235222F9817B}.Release|Any CPU.Build.0 = Release|Any CPU
{EAD2138A-1553-43A9-B51F-55FC2A2CEFFD}.Release|Any CPU.ActiveCfg = Release|Any CPU
{EAD2138A-1553-43A9-B51F-55FC2A2CEFFD}.Release|Any CPU.Build.0 = Release|Any CPU
{690312C5-1948-4530-832D-6332625D4E9C}.Release|Any CPU.ActiveCfg = Release|Any CPU
diff --git a/Utility/Tax/TaxUtility.cs b/Utility/Tax/TaxUtility.cs
index 44d2619..069349f 100644
--- a/Utility/Tax/TaxUtility.cs
+++ b/Utility/Tax/TaxUtility.cs
@@ -25,7 +25,7 @@ public TaxUtility(decimal singleTaxRate)
/// Note that tax rates must be expressed as a percentage number, not a fraction.
public TaxUtility(IEnumerable> taxRatesAsPercentageHistory)
{
- Precondition.Requires(taxRatesAsPercentageHistory!=null!);
+ Contract.Requires(taxRatesAsPercentageHistory!=null!);
_taxValues = new ValueChangesListProvider(taxRatesAsPercentageHistory);
}
diff --git a/Utility/VaryingValues/ValueChangesListProvider.cs b/Utility/VaryingValues/ValueChangesListProvider.cs
index 2f5db4d..0b4ae6d 100644
--- a/Utility/VaryingValues/ValueChangesListProvider.cs
+++ b/Utility/VaryingValues/ValueChangesListProvider.cs
@@ -19,7 +19,7 @@ public class ValueChangesListProvider : IVaryingValuePro
///
public ValueChangesListProvider(IEnumerable> valuesAcrossRange)
{
- Precondition.Requires(valuesAcrossRange!=null!);
+ Contract.Requires(valuesAcrossRange!=null!);
InitialiseFrom(valuesAcrossRange.ToList());
}
@@ -29,7 +29,7 @@ public ValueChangesListProvider(IEnumerable>
///
public ValueChangesListProvider(ValueChange singleValue)
{
- Precondition.Requires(singleValue!=null!);
+ Contract.Requires(singleValue!=null!);
InitialiseFrom( new List> { singleValue } );
}
@@ -40,7 +40,7 @@ public ValueChangesListProvider(ValueChange singleValue)
/// The name of the configuration section, eg 'TaxHistory'
public ValueChangesListProvider(IConfiguration configuration, string sectionName)
{
- Precondition.Requires(configuration!=null!);
+ Contract.Requires(configuration!=null!);
List> valuesInConfig = new List>();
configuration.Bind(sectionName, valuesInConfig);
InitialiseFrom(valuesInConfig);
@@ -52,7 +52,7 @@ public ValueChangesListProvider(IConfiguration configuration, string sectionName
///
public ValueChangesListProvider(IConfigurationSection valueChangesSection)
{
- Precondition.Requires(valueChangesSection!=null!);
+ Contract.Requires(valueChangesSection!=null!);
List> valuesInConfig = new List>();
valueChangesSection.Bind(valuesInConfig);
InitialiseFrom(valuesInConfig);
@@ -60,7 +60,7 @@ public ValueChangesListProvider(IConfigurationSection valueChangesSection)
private void InitialiseFrom(List> valuesAcrossRange)
{
- Precondition.Requires(valuesAcrossRange!=null!);
+ Contract.Requires(valuesAcrossRange!=null!);
_valueChangesInOrder = valuesAcrossRange.OrderBy(c => c.From).ToList();
}