Skip to content

TZif is an Ada 2022 library for parsing and querying IANA's compiled timezone information (TZif format, RFC 9636).

License

Notifications You must be signed in to change notification settings

abitofhelp/tzif_ada

Repository files navigation

IANA Timezone Information File Library

License Ada Alire SPARK

Version: 3.0.3
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

Note: A companion library providing higher-level functions for working with timezones and durations in Ada 2022 will be released soon.

Overview

TZif is an Ada 2022 library for parsing and querying IANA's compiled timezone information (TZif format, RFC 9636) files. It provides a clean, functional API with Result monad error handling, hexagonal architecture, and embedded-safe patterns.

Designed for safety-critical, embedded, and high-assurance applications with full SPARK compatibility.

Features

  • Parse IANA TZif binary files (versions 1, 2, and 3)
  • Query timezone transitions at any Unix epoch time
  • Discover and validate timezone data sources
  • Find zones by ID, pattern, region, or regex
  • Detect the system's local timezone
  • Cross-platform: Linux, macOS, BSD, Windows 11, Embedded
  • 4-layer hexagonal architecture (Domain, Application, Infrastructure, API)
  • Result monad error handling (via functional ^4.0.0)
  • Generic I/O plugin pattern for platform portability
  • Smart constructor pattern with Functional.Try.Map_To_Result

SPARK Formal Verification

Status SPARK Proved
Scope Domain + Application layers (value objects, containers, parser, operations, ports)
Mode gnatprove --mode=prove --level=2
Results See CHANGELOG for current proof statistics

The domain and application port layers are formally verified using SPARK Ada, providing mathematical guarantees of:

  • No runtime errors - Division by zero, overflow, range violations
  • No uninitialized data - All variables properly initialized before use
  • Contract compliance - Pre/postconditions proven correct
  • Data flow integrity - No aliasing or information flow violations

Verification Commands

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

SPARK Layer Coverage

Layer SPARK_Mode Description
Domain On Value objects, bounded containers, parser, error types
Application On Operations, inbound ports, outbound ports
Infrastructure Off I/O operations (file system, platform)
API Off Facade over infrastructure

Getting Started

Clone with Submodules

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

Or if already cloned:

git submodule update --init --recursive

Building

# Build the library
make build

# Build release version
make build-release

Using in Your Project

Add to your alire.toml:

[[depends-on]]
tzif = "^3.0.3"

Quick Example

with Ada.Text_IO; use Ada.Text_IO;
with TZif.API;

procedure Show_Local_Timezone is
   use TZif.API;
   Result : constant My_Zone_Result := Find_My_Id;
begin
   if Is_Ok (Result) then
      Put_Line ("Local timezone: " & To_String (Value (Result)));
   else
      Put_Line ("Could not detect local timezone");
   end if;
end Show_Local_Timezone;

API Operations

TZif provides 11 operations through TZif.API:

Operation Description
Find_By_Id Lookup timezone by exact IANA identifier
Find_By_Pattern Search zones by substring match
Find_By_Region Search zones by geographic region
Find_By_Regex Search zones using regular expressions
Find_My_Id Detect the system's local timezone
Get_Transition_At_Epoch Query UTC offset and DST at any time
Get_Version Retrieve IANA database version
List_All_Zones Enumerate all available timezones
Discover_Sources Find timezone data directories
Load_Source Load a specific timezone data source
Validate_Source Validate timezone data integrity

Architecture

+-----------------------------------------------------------------+
|                          API Layer                               |
|  TZif.API (facade) + TZif.API.Desktop/Windows/Embedded (roots)  |
+----------------------------------+------------------------------+
                                   |
+----------------------------------v------------------------------+
|                      Application Layer                           |
|  Use Cases (11 operations) + Inbound/Outbound Ports             |
+----------------------------------+------------------------------+
                                   |
+----------------------------------v------------------------------+
|                    Infrastructure Layer                          |
|  I/O Adapters (Desktop, Windows, Embedded) + Platform Ops       |
+----------------------------------+------------------------------+
                                   |
+----------------------------------v------------------------------+
|                       Domain Layer                               |
|  Entities (Zone) + Value Objects + Parser + Result Monad        |
+-----------------------------------------------------------------+

Platform Support

Platform Status Timezone Source
Linux Full /usr/share/zoneinfo
macOS Full /var/db/timezone/zoneinfo
BSD Full /usr/share/zoneinfo
Windows Full User-provided IANA tzdata + Win32 API
Embedded Stub Custom adapter required

Testing

# Run all tests
make test-all

# Run unit tests only
make test-unit

# Run integration tests only
make test-integration

Test Results: All tests passing. See CHANGELOG for current counts.

Documentation

Examples

The examples/ directory contains 11 working programs:

Example Description
discover_sources Find timezone sources
find_by_id Find timezone by exact ID
find_by_pattern Search zones by substring
find_by_region Search zones by region
find_by_regex Search zones by regex
find_my_id Detect system's local timezone
get_transition_at_epoch Query offset at specific time
get_version Query database version
list_all_zones Enumerate all zones
load_source Load timezone source
validate_source Validate source integrity
# Build and run examples
make build-examples
./bin/examples/find_by_id

Dependencies

Package Version Purpose
functional ^4.0.0 Result/Option monads, Functional.Try
gnatcoll ^25.0.0 GNAT Components Collection

Note: Domain layer has zero external dependencies (pure Ada 2022).

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
# Initialize submodules
make submodule-init

# Update submodules
make submodule-update

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 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 (v3.0.3)

  • TZif v1/v2/v3 binary parsing (RFC 9636)
  • 4-layer hexagonal architecture
  • Public API facade with stable interface
  • Cross-platform: POSIX and Windows
  • SPARK formal verification (see CHANGELOG)
  • Comprehensive test coverage (see CHANGELOG)
  • Comprehensive documentation
  • 11 example programs
  • Smart constructor pattern with Functional.Try

About

TZif is an Ada 2022 library for parsing and querying IANA's compiled timezone information (TZif format, RFC 9636).

Topics

Resources

License

Stars

Watchers

Forks

Sponsor this project

 

Packages

No packages published