Skip to content

A high-performance, type-safe Ada library for handling time zones using the IANA Time Zone Database. Built with modern software engineering practices including Domain-Driven Design, Clean Architecture, and comprehensive contract-based programming.

License

Notifications You must be signed in to change notification settings

abitofhelp/zoneinfo_ada

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

55 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

IANA Timezone Datetime Manipulation Library for Ada 2022

License Ada SPARK Alire

Version: 1.1.1
Date: 2025-12-16
SPDX-License-Identifier: BSD-3-Clause
License File: See the LICENSE file in the project root
Copyright: © 2025 Michael Gardner, A Bit of Help, Inc.
Status: Released

Overview

Zoneinfo is an IANA timezone datetime manipulation library for Ada 2022. Built on the TZif library for IANA database access, it provides a clean, type-safe API for working with timezones, parsing ISO 8601 strings, formatting datetimes, and discovering timezone sources. The library follows hybrid DDD/Clean/Hexagonal architecture with functional error handling and is designed for both desktop and embedded platforms.

Features

  • Timezone-Aware Datetimes - Instant, Zoned, and Civil time representations
  • ISO 8601 Parsing - Parse datetime strings with timezone offsets and zone IDs
  • Datetime Formatting - Format datetimes as ISO 8601 or custom patterns
  • Timezone Discovery - Find system timezone, search by pattern/region/regex (bounded arrays)
  • Duration Arithmetic - Add/subtract durations, calculate differences
  • TZif Integration - Built on the TZif library for IANA timezone database access
  • Result Monad Error Handling - No exceptions, functional error handling
  • 4-Layer Hexagonal Architecture - Domain -> Application -> Infrastructure -> API
  • SPARK Verified - Domain + Application layers formally verified
  • Embedded Safety - No implicit heap allocations, bounded types, static dispatch
  • Library Standalone - Explicit Library_Interface for ABI stability

SPARK Formal Verification

Status SPARK Proved
Scope Domain + Application Layers
Mode gnatprove --mode=prove --level=2
Results See CHANGELOG for current verification statistics

The domain and application layers are formally verified using SPARK Ada, ensuring:

  • No uninitialized data - All variables properly initialized before use
  • Data flow integrity - No aliasing or information flow violations
  • Contract consistency - Pre/postconditions are consistent

Infrastructure and API layers use SPARK_Mode => Off as they perform I/O operations and TZif integration.

Verification Commands

make spark-check    # Run SPARK legality verification
make spark-prove    # Run full SPARK proof verification

SPARK Coverage

Layer SPARK_Mode Description
Domain On Value objects (Instant, Zoned, Civil, Duration, Zone_ID), 7-operation Result
Application On Use cases and ports
Infrastructure Off I/O operations, TZif adapters
API Off Facade over infrastructure

Getting Started

Clone with Submodules

This repository uses git submodules for shared tooling. Clone with:

git clone --recurse-submodules https://github.com/abitofhelp/zoneinfo.git

Or if already cloned without submodules:

git submodule update --init --recursive
# Or: make submodule-init

Architecture

+-------------------------------------------------------------+
|                      Zoneinfo.API                           |
|              (Public Facade - Stable Interface)             |
+-------------------------------------------------------------+
|  API.Operations  |  API.Parse  |  API.Format  | API.Discovery|
|  (Pure ops)      |  (ISO 8601) |  (Display)   | (TZ sources) |
+-------------------------------------------------------------+
|                    Application Layer                        |
|         Use Cases  |  Ports (Timezone)  |  Commands         |
+-------------------------------------------------------------+
|                   Infrastructure Layer                      |
|         Adapters (TZif Integration, Discovery)              |
+-------------------------------------------------------------+
|                      Domain Layer                           |
|  Instant | Zoned | Civil | Duration | Zone_ID | Source_Info |
|  Zone_List | Search_Results | 7-operation Result            |
+-------------------------------------------------------------+

Quick Start

Building

# Build debug library
make build

# Build release library
make build-release

# Using Alire directly
alr build

Using in Your Project

Add to your alire.toml:

[[depends-on]]
zoneinfo = "^1.1.1"

In your Ada code:

with Zoneinfo.API;
with Zoneinfo.API.Parse;
with Zoneinfo.API.Format;
use Zoneinfo.API;

procedure Main is
   --  Parse ISO 8601 string
   Parse_Result : constant Civil_Result.Result :=
     Parse.From_ISO_8601 ("2025-12-15T14:30:00");

   --  Create a timezone
   Zone_Result : constant Zone_ID_Result.Result :=
     Zone_ID_Pkg.From_String ("America/New_York");

   --  Create duration
   One_Hour : constant Duration_Type :=
     Duration_Pkg.From_Hours (1);

   --  Format datetime
   Formatted : constant String :=
     Format.To_String (Format.To_ISO_8601 (Some_Civil_Time));
begin
   if Civil_Result.Is_Ok (Parse_Result) then
      --  Success! Use the parsed Civil time
      null;
   else
      --  Handle error
      null;
   end if;
end Main;

Usage Examples

Working with Timezones

with Zoneinfo.API;
use Zoneinfo.API;

--  UTC is a convenience constant (no Result unwrapping needed)
Zone : constant Zone_ID := UTC;

--  Create instant (epoch nanoseconds)
Now : constant Instant := Instant_Pkg.From_Epoch_Nanos (1700000000);

--  Create zoned datetime
Zoned_Time : constant Zoned := Zoned_Pkg.Create (Now, Zone);

--  Change timezone (preserves instant)
NY_Result : constant Zone_ID_Result.Result :=
  Zone_ID_Pkg.From_String ("America/New_York");

if Zone_ID_Result.Is_Ok (NY_Result) then
   declare
      NY_Zone : constant Zone_ID := Zone_ID_Result.Value (NY_Result);
      NY_Time : constant Zoned := Zoned_Pkg.With_Zone (Zoned_Time, NY_Zone);
   begin
      --  NY_Time has same instant, different timezone context
      null;
   end;
end if;

Parsing ISO 8601

with Zoneinfo.API.Parse;

--  Parse datetime
Result := Parse.From_ISO_8601 ("2025-12-15T14:30:00");

--  Parse with offset
Result := Parse.From_ISO_8601_With_Offset ("2025-12-15T14:30:00-05:00");

--  Parse with zone
Result := Parse.From_ISO_8601_With_Zone ("2025-12-15T14:30:00[America/New_York]");

--  Parse duration
Duration_Result := Parse.From_ISO_Duration ("PT1H30M");

Formatting

with Zoneinfo.API.Format;

--  Format returns Datetime_String (bounded); use To_String to convert
ISO_Bounded : constant Format.Datetime_String :=
  Format.To_ISO_8601 (Civil_Time);
ISO_String  : constant String := Format.To_String (ISO_Bounded);

--  Format date portion only
Date_Only : constant Format.Datetime_String := Format.To_ISO_Date (Civil_Time);

--  Format with offset
With_Offset : constant Format.Datetime_String :=
  Format.To_ISO_8601_With_Offset (Civil_Time, UTC_Offset);

Timezone Discovery (v1.1.0 Bounded Arrays)

with Zoneinfo.API.Discovery;

--  Find system timezone
My_Zone : constant Zone_ID_Result.Result := Discovery.Find_My_Id;

--  Discover timezone sources
Paths : Path_List (1 .. 1);
Paths (1) := Make_Path ("/usr/share/zoneinfo");
Source_Result : constant Source_Info_Result.Result :=
  Discovery.Discover_Sources (Paths);

--  List all zones (returns bounded Zone_List, not callback)
if Source_Info_Result.Is_Ok (Source_Result) then
   declare
      Source : constant Source_Info := Source_Info_Result.Value (Source_Result);
      Zones_Result : constant Zone_List_Result.Result :=
        Discovery.List_All_Zones (Source);
   begin
      if Zone_List_Result.Is_Ok (Zones_Result) then
         declare
            Zones : constant Zone_List := Zone_List_Result.Value (Zones_Result);
         begin
            --  Iterate bounded array
            for I in 1 .. Zones.Count loop
               Process_Zone (Zones.Items (I));
            end loop;
         end;
      end if;
   end;
end if;

--  Search by pattern (returns bounded Search_Results)
Pattern_Result : constant Search_Results_Result.Result :=
  Discovery.Find_By_Pattern ("York", Source);

if Search_Results_Result.Is_Ok (Pattern_Result) then
   declare
      Results : constant Search_Results :=
        Search_Results_Result.Value (Pattern_Result);
   begin
      for I in 1 .. Results.Count loop
         --  Each result contains the matching Zone_ID
         Process_Zone (Results.Items (I));
      end loop;
   end;
end if;

Testing

# Run all tests
make test-all

# Build tests
make build-tests

# Run unit tests only
./test/bin/unit_runner

# Run integration tests only
./test/bin/integration_runner

Test Results: All 489 tests passing (335 unit + 154 integration)

Documentation

Code Standards

This project follows:

  • Ada Agent (~/.claude/agents/ada.md) - Ada 2022 standards
  • Architecture Agent (~/.claude/agents/architecture.md) - DDD/Clean/Hexagonal
  • Functional Agent (~/.claude/agents/functional.md) - Result/Option patterns
  • SPARK Agent (~/.claude/agents/spark.md) - Formal verification patterns

Submodule Management

This project uses git submodules for shared tooling:

  • docs/common - Shared documentation templates and guides
  • scripts/python - Build, release, and architecture scripts
  • test/python - Shared test fixtures and configuration

Commands

# After fresh clone
make submodule-init

# Pull latest from submodule repos
make submodule-update

# Check current submodule commits
make submodule-status

Dependencies

Dependency Version Purpose
gnat >=13 Ada 2022 compiler
gnatcoll ^25.0.0 GNAT components collection
functional ^4.0.0 Result monad and functional patterns
tzif ^3.0.3 IANA timezone database access

Contributing

This project is not open to external contributions at this time.

AI Assistance & Authorship

This project - including its source code, tests, documentation, and other deliverables - is designed, implemented, and maintained by human developers, with Michael Gardner as the Principal Software Engineer and project lead.

We use AI coding assistants (such as OpenAI GPT models and Anthropic Claude Code) as part of the development workflow to help with:

  • drafting and refactoring code and tests,
  • exploring design and implementation alternatives,
  • generating or refining documentation and examples,
  • and performing tedious and error-prone chores.

AI systems are treated as tools, not authors. All changes are reviewed, adapted, and integrated by the human maintainers, who remain fully responsible for the architecture, correctness, and licensing of this project.

License

Copyright (c) 2025 Michael Gardner, A Bit of Help, Inc.

Licensed under the BSD-3-Clause License. See LICENSE for details.

Author

Michael Gardner
A Bit of Help, Inc.
https://github.com/abitofhelp

Project Status

Status: Released (v1.1.1)

  • Core timezone-aware datetime types (Instant, Zoned, Civil)
  • ISO 8601 parsing and formatting
  • Timezone discovery with bounded arrays (SPARK-compatible)
  • Duration arithmetic and comparisons
  • TZif library integration (v3.0.3)
  • 4-layer hexagonal architecture
  • Full test suite (489 tests)
  • Comprehensive documentation
  • SPARK legality verification for Domain + Application layers
  • Alire publication

About

A high-performance, type-safe Ada library for handling time zones using the IANA Time Zone Database. Built with modern software engineering practices including Domain-Driven Design, Clean Architecture, and comprehensive contract-based programming.

Topics

Resources

License

Stars

Watchers

Forks

Sponsor this project

 

Packages

No packages published