Formal Methods vs. Plain Text Descriptions in Software Engineering

Introduction

In software engineering, how we define system behavior can make the difference between a reliable application and one riddled with bugs. Two common approaches are:

1. Plain text descriptions (natural language, user stories).
2. Formal methods (mathematical modeling, logic-based specifications).

This post compares them and shows which one results in LLMs generating a better code when we input these descriptions.

Plain Text Descriptions: The Agile Standard

Plain text descriptions use natural language to define requirements. Examples:

• User stories (“As a user, I want to log in to a service”).
• Acceptance criteria (“The authorizations service must be able to handle 10,000 concurrent requests”).

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81package main

import (
	"errors"
	"fmt"
)

type User struct {
	ID       string
	Username string
	LoggedIn bool
}

type Product struct {
	ID    string
	Name  string
	Price float64
}

type CartItem struct {
	Product  Product
	Quantity int
}

type Cart struct {
	userID string
	items  map[string]CartItem
}

type CartManager struct {
	carts map[string]*Cart
}

func NewCartManager() *CartManager {
	return &CartManager{
		carts: make(map[string]*Cart),
	}
}

func (cm *CartManager) GetCart(userID string) *Cart {
	if cart, exists := cm.carts[userID]; exists {
		return cart
	}

	cart := &Cart{
		userID: userID,
		items:  make(map[string]CartItem),
	}
	cm.carts[userID] = cart
	return cart
}

func (c *Cart) AddToCart(product Product) error {
	if item, exists := c.items[product.ID]; exists {
		item.Quantity++
		c.items[product.ID] = item
	} else {
		c.items[product.ID] = CartItem{
			Product:  product,
			Quantity: 1,
		}
	}
	return nil
}

func (c *Cart) GetItems() []CartItem {
	items := make([]CartItem, 0, len(c.items))
	for _, item := range c.items {
		items = append(items, item)
	}
	return items
}

func handleAddToCart(user *User, product Product, cartManager *CartManager) error {
	if !user.LoggedIn {
		return errors.New("please log in to add items to your cart")
	}

	cart := cartManager.GetCart(user.ID)
	return cart.AddToCart(product)
}
copy

Formal Methods: Precision Through Math

Formal methods use mathematical logic to specify and verify systems.

Formal Method Example

Activity diagram (though UML is not exactly formal) for the textual description mentioned above:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
+
30
31
32
33
+
35
36
37
38
39
40
41
42
43
+
+
46
47
48
49
50
51
52
53
54
55
56
57
58
59
+
+
62
63
64
65
66
67
68
69
70
71
72
73
74
75
+
+
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93package main

import (
	"errors"
	"fmt"
	"sync"
)

type User struct {
	ID       string
	Username string
	LoggedIn bool
}

type Product struct {
	ID    string
	Name  string
	Price float64
}

type CartItem struct {
	Product  Product
	Quantity int
}

type Cart struct {
	userID string
	items  map[string]CartItem
	mu     sync.Mutex 
}

type CartManager struct {
	carts map[string]*Cart
	mu    sync.Mutex 
}

func NewCartManager() *CartManager {
	return &CartManager{
		carts: make(map[string]*Cart),
	}
}

func (cm *CartManager) GetCart(userID string) *Cart {
	cm.mu.Lock() 
	defer cm.mu.Unlock() 

	if cart, exists := cm.carts[userID]; exists {
		return cart
	}

	cart := &Cart{
		userID: userID,
		items:  make(map[string]CartItem),
	}
	cm.carts[userID] = cart
	return cart
}

func (c *Cart) AddToCart(product Product) error {
	c.mu.Lock() 
	defer c.mu.Unlock() 

	if item, exists := c.items[product.ID]; exists {
		item.Quantity++
		c.items[product.ID] = item
	} else {
		c.items[product.ID] = CartItem{
			Product:  product,
			Quantity: 1,
		}
	}
	return nil
}

func (c *Cart) GetItems() []CartItem {
	c.mu.Lock() 
	defer c.mu.Unlock() 

	items := make([]CartItem, 0, len(c.items))
	for _, item := range c.items {
		items = append(items, item)
	}
	return items
}

func handleAddToCart(user *User, product Product, cartManager *CartManager) error {
	if !user.LoggedIn {
		return errors.New("please log in to add items to your cart")
	}

	cart := cartManager.GetCart(user.ID)
	return cart.AddToCart(product)
}
copy

Key Differences at a Glance