Thoughts dump — Software Abstractions

Thoughts dump — Software Abstractions

I was given a recommendation for the book Software Abstractions — and a 10-minute reading intrigued me. This weekend, I spent a bit more time dabbling on the topic and tried out some of the examples. This is a dump of what I’ve understood software.

My goal is to be more precise in software modeling. I know from SWE experience at least that defects in software models — how the real world is represented in our systems — results in software complexity. Unnecessary complexity makes our software brittle — easily breaks when changed — which eventually lead to costly migrations, rewrites, or early decommissions.

Despite these concerns, software modeling itself is not usually an area I heavily invest in. I invest a lot in ensuring engineers in my team get as much context as possible through strategic DDD — poor understanding of the context is a ticket to poor modeling. Once a model has been created, I also invest a lot in the team’s ability to refactor — through a high unit test coverage, clean code, YAGNI, and all that good stuff. The modeling process itself, however, is only a creative exercise, usually done in a couple hours. Perhaps mob designing is the only initiative I’ve used to guarantee the output of higher-quality models.

The promise of the book to make rigorous the process of software modeling itself intrigues me. The following quote immediately drew my attention:

When you want to rework a constraint in the model, you can ask the analyzer to check that the new and old constraint have the same meaning. This is like using unit tests to check refactoring in code, except that the analyzer typically checks billions of cases, and there are no test suites to write.

Having been recently introduced to TDD, I experienced how continuously testing the code I write improves the quality and minimizes bloat. If this method could do the same for modeling, it would be a game-changer.

The book presents three things:

• A logical framework to represent structures formally.
• A precise modeling language, called Alloy.
• A simulator, Alloy Analyzer.

The book cuts to chase and immediately introduces a walk-through with Alloy and Alloy analyzer in the first chapter — A Whirlwind Tour. It presents the example of modeling address book. The way the model is fully shaped is similar to TDD, although the book doesn’t stress on being test-first. We add constraints on the basic model as we add predicates or evolve the model properties. Then, we run the simulator against our evolved constraints/model and check if the simulator finds either:

• any counterexample against an assertion that should stand
• zero matches of an instance that satisify the model properties for a particular level of depth.

If we find neither issue, we gain confidence that our model is robust — against the constraints we defined. Or we can crank up the “depth” and the simulator will attempt to generate more instances and see if a counterexample is found.

There is no way I can explain the concepts as well as the book, but here is a snippet from the book that I tried:

sig Name, Addr {}
sig Book {
 addr: Name ->lone Addr
}
pred show (b: Book) {
 // constraints filled given the structure
 #b.addr > 1
 #Name.(b.addr) > 1

 // this constraint is not possible to be fulfilled, since one Name maps to one Address (lone)
 some n: Name | #n.(b.addr) > 1
}
pred add(b, newB: Book, n: Name, a: Addr) {
 newB.addr = b.addr + n-> a
}

pred showAdd(b, newB: Book, n: Name, a: Addr) {
 add [b, newB, n, a] // the book uses () parentheses, but v6.0 of Alloy throws syntax error and works with square bracket instead []
 #Name.(newB.addr) > 1
}

// only one of the run will execute, need to comment the other one
run show for 3 but 1 Book // simulate with up to 3 addr instances and 1 book
run showAdd for 3 but 2 Book // simulate up to 3 addr instances and 1 book

The next chapter is however a challenge for me to digest — I am not (or no longer) familiar enough with the notation and math logic to follow along 😆. I would love to learn more interactively and try my own examples, but I found that I know too little of the syntax and the style of modeling to do so. Here’s my failed attempt at modeling a cart/product:

module learning/coratCoret1

sig Quantity {
 amount: Int
}
sig Product {}
sig Cart {
 item: Product ->lone Quantity
}

pred show(c: Cart) {
 #c.item > 1
 #Product.(c.item) > 1
}

pred addOne(c, cnew: Cart, p: Product, q: Quantity) {
  let existingQuantity = c.item. |
    cnew.item = (c.item - p->existingQuantity) + p->(existingQuantity + q)
}

run addOne for 3 but 1 Cart

I want to model a combined quantity when a product is added to the cart and the product is already in the cart. But I can’t get the syntax right so far — and I doubt I should be representing the amount as Int.

This is as far as I go for now. My current impression is still that this should be very useful in areas where we need to ensure minimum modeling issues (i.e. almost all modeling past a certain scale haha). Once a precise ubiquitous language is starting to take shape, I imagine engineers can use this approach to provide incredibly rapid feedback to product teams about what edge cases/counterexamples might arise in a design.

Hope I can learn more on this topic!