Converting programming logic to mathematical notation

How do I go about converting programming logic to mathematic notation?

For example, I read a question that asks:

A piece of software is set to run every 35 minutes. The time is now 2.03pm. The software last ran at 1.25pm. Write a solution that checks to see if the software needs to be ran.

Easy enough. First convert the current time, and last run time, to timestamps. Add 35 minutes to the last ran timestamp and check if this time is less than the current time.

if((last_run_ts + 35 minutes) <= current_time_ts)
    run_software()

I was curious on how I would express this in mathematical notation? I know that a lot of algorithms are first written in mathematical notation, and converted to programming code afterwards. I've never had to do this personally.

And where can I learn more about this? Would most of this be discrete mathematics?

Solution 1:

Actually, your example contains much more than programming logic. You start with some requirements on the software described using real-world notions like time and then you give some fragments of code that could help to implement those requirements.

Constructing formal mathematical models for expressing requirements and implementations is a topic that is generally referred to as formal methods in computer science. There is lot of literature on this (see the link).

In examples like yours, formal methods make you be much more precise about what the requirements mean and about whether an implementation meets the requirements. In your example, building a precise mathematical model would force you to think about important issues: you say it is "easy enough", but what if the problem is posed in the context of a software system that is distributed over multiple servers in many different physical locations?