This post explores what TLA+ is and why it may be worth using.

What is TLA+?

How do you know that your code works? Traditionally, there have been two options: you can prove it using mathematics; or you can write tests to show that despite your best effort you cannot break it.

Proving vs Testing

Postman environment variables can actually contain other variables.  In this post we explore how to leverage this feature, and discuss possible use cases.

Nested environment variables in Postman

Access modifiers control whether a type (e.g., a class), or one of its properties can be used by other code.  A public class, for instance, can be used by any code in any assembly.  In this post we explore how the internal access modifier can provide a mechanism for enforcing boundaries in our architecture.

Access modifiers

On a previous post we defined software architecture as a set of rules for defining the components of a system, and for how those components interact with each other. Now we explore why software architecture can influence how a system evolves over time impacting its maintainability.

Why care about architecture?

PlusCal is a language for writing algorithms that translates into TLA+.  It is an invaluable tool for reasoning about concurrency.

PlusCal

Writing good unit tests is hard.  Ideally we use as little code as possible to cover as many use cases as possible.  One tool to help with this challange is data driven tests.

Data driven tests

What must be true of every state in all behaviors of a functioning traffic light?

Modeling a traffic light - Part 4: Invariants

What does a TLA+ specification look like?

Modeling a traffic light - Part 3: Specification

EF core 7.0 introduces a new, more efficient way of upating one or more properties of several entities.

Entity Framework Bulk Update

This drill consists of running two Docker containers: one for an API app, the other for a database.

Docker Drill

Window functions allow you to answer interesting questions about your data.  In this post we are going to look at the RANK and DENSE_RANK functions in particular.

SQL Window Functions: RANK and DENSE_RANK

How to build a docker image when some NuGet packages are in a private Azure Artifacts feed.

Private Azure Artifacts feed and Docker

I think of a drill as a small exercise you do every now and then to keep yourself sharp.  This drill is about using pivot in SQL.

SQL Drill: Pivot

This post introduces the concept of behavior in TLA+.

Modeling a traffic light - Part 2: Behavior

This post explores how to leverage Azure Service Bus and Azure Functions to create a workflow framework capable of handling proccesses spanning multiple services.

Processes across multiple services: A better approach

A system typically has use cases requiring coordination between multiple services. When selling a product, for example, an ecommerce site may use several services to bill, deliver to, and communicate with the client.  This post discusses a possible way to execute this type of use case.

Processes across multiple services

In the prior post we saw that LINQ does not provide an equivalent to the method SymmetricExceptWith.  How would you implement an equivalent using only LINQ methods?

SymmetricExceptWith using LINQ

A set is an unordered collection containing no duplicates. Common operations on sets include intersection, difference, and union.  C# provides at least two ways of performing these operations: one is using LINQ extensions; the other, is Hashset, a generic collection.

Sets in C#

When modeling a system we have to determine how we are going to represent its state.  In this post we explore how to do that for a traffic light.

Modeling a traffic light - Part 1: State

In this post we explore how to generate data before sending a request, and how to store that data in the environment so that it can be used by other requests.

Generating data before sending a request

Microservices and monoliths are often presented as polar opposites.  But microservices, monoliths and everything in between are attempting to solve the same problem: how best to write software?  Software architecture describes what answers to this question share in common.

What is software architecture?

Postman is a powerful tool for testing and exploring APIs.  This post shows how to create a collection that passes values between requests using environment variables.  This technique is helpful for sharing workflows with members of your team.

All Posts

What is TLA+?

Proving vs Testing

Nested environment variables in Postman

Access modifiers

Why care about architecture?