AlgorithmsAreCool

newtype ThreadId = i: nat | i <= 0xffff_ffff

class Lock
{
    static const NULL_THREAD_ID : ThreadId := 0

    var ownerThread : ThreadId

    constructor()
        ensures ownerThread == NULL_THREAD_ID

AlgorithmsAreCool

type Timestamp = t: int| 0 <= t <= 9223372036854775808 //2^63

class Entity
{
    var id : string

    predicate isEqual(other : Entity)
        reads this, other
    {
        id == other.id

AlgorithmsAreCool

service ControlPlane {
  rpc QueryUsage (QueryConsumptionRequest) returns (QueryConsumptionResponse) {}
  rpc RegisterHandler (RegisterHandlerRequest) returns (RegisterHandlerResponse) {}
}

AlgorithmsAreCool

// See https://aka.ms/new-console-template for more information
using CsCheck;


Console.WriteLine("Hello, World!");

TestIteratedDirectIntegerSpaceCoverage();

void TestEnumeratedSpaceCoverage()
{

AlgorithmsAreCool

let sum = [1..10] |> List.reduce (+)

AlgorithmsAreCool

using System;
using System.Collections.Generic;
using System.Diagnostics;
using System.Threading;
using System.Threading.Tasks;

namespace BatchedAwait
{
    
    public static class EntryPoint

AlgorithmsAreCool

Examples of Sugar since C# 6.0

• Discards
• ?.
• Dictionary Initializers
• Auto-Property Initializers (heck, Auto Properties in general)
• Using Static
• Inline out variables
• Async Main
• Non-trailing named arguments

AlgorithmsAreCool

using System;
using System.Collections.Concurrent;

using System.Threading;
using System.Threading.Channels;
using System.Threading.Tasks;

namespace HomebrewDataflow
{
    public abstract class WorkflowStageBase<TIn>

AlgorithmsAreCool

using System;

using System.Threading;
using System.Threading.Tasks;
using System.Threading.Tasks.Dataflow;

namespace randomTPLRepro
{
    class Program
    {

AlgorithmsAreCool

Project File

<Project Sdk="Microsoft.NET.Sdk">

  <PropertyGroup>
    <OutputType>Exe</OutputType>
    <TargetFramework>netcoreapp3.0</TargetFramework>
  </PropertyGroup>

  <ItemGroup>