simple_eif_phone

Write an Android app in Eiffel, and get a signed APK from one command.

MIT License Android 8.0 or later Design by Contract

API Reference

Generated from the source, so the contracts here are the ones the code runs. PHONE_NATIVE is left out: nothing in it is public.

SIMPLE_EIF_PHONE

The app's one handle on the phone. Eiffel owns the loop: `wait_for_event' / `poll_event' deliver `last_event', and before they return, `lifecycle' and `touches' have already applied it. There are no callbacks into Eiffel: the C glue queues, Eiffel pulls. One handle per process; when the app's root returns, the glue finishes the activity and ends the process (research D-012).

Constants

Back_system: INTEGER = 0

Android also handles Back (finishes the app); the key is still delivered.

Back_app: INTEGER = 1

Back is consumed; only the app reacts.

Events

wait_for_event

Block until an event arrives; it becomes `last_event'.

Requires

not_destroyed: not lifecycle.is_destroyed no_open_frame: not screen.in_frame

Ensures

delivered: not last_event.is_none counted: delivery_count = old delivery_count + 1 fresh_event: last_event /= old last_event kind_from_c: last_event.kind = c_cur_kind lifecycle_in_step: lifecycle.last_applied = last_event touches_in_step: touches.last_applied = last_event metrics_refreshed: is_metric_kind (last_event.kind) implies (metrics.width = screen.width and metrics.height = screen.height) drops_monotonic: dropped_event_count >= old dropped_event_count

poll_event (a_timeout_ms: INTEGER)

Wait at most `a_timeout_ms'; `last_event' is none on timeout.

Requires

timeout_ok: a_timeout_ms >= 0 not_destroyed: not lifecycle.is_destroyed no_open_frame: not screen.in_frame

Ensures

counted_when_delivered: not last_event.is_none implies delivery_count = old delivery_count + 1 nothing_taken_on_timeout: last_event.is_none implies delivery_count = old delivery_count kind_from_c: not last_event.is_none implies last_event.kind = c_cur_kind lifecycle_in_step: not last_event.is_none implies lifecycle.last_applied = last_event touches_in_step: not last_event.is_none implies touches.last_applied = last_event metrics_refreshed: is_metric_kind (last_event.kind) implies (metrics.width = screen.width and metrics.height = screen.height) timeout_changes_nothing: last_event.is_none implies (lifecycle.last_applied = old lifecycle.last_applied and touches.last_applied = old touches.last_applied) drops_monotonic: dropped_event_count >= old dropped_event_count

delivery_count: INTEGER

Events delivered so far (the C side's count of taken events).

Ensures

non_negative: Result >= 0

is_metric_kind (a_k: INTEGER): BOOLEAN

Does an event of kind `a_k' make `metrics' re-read Android?

last_event: PHONE_EVENT

Most recent delivery (none before the first, or after a timeout).

dropped_event_count: INTEGER

Touch moves dropped on queue overflow so far (never lifecycle or key events).

Ensures

non_negative: Result >= 0

State

lifecycle: PHONE_LIFECYCLE

Where the app is in Android's life, including `last_event'.

touches: PHONE_TOUCHES

Fingers down, including `last_event'.

handle_exists: BOOLEAN

Has this process claimed its platform handle?

Services

screen: PHONE_SCREEN

metrics: PHONE_METRICS

storage: PHONE_STORAGE

assets: PHONE_ASSETS

log: PHONE_LOG

Behavior

back_policy: INTEGER

`Back_system' or `Back_app' (read from the C side, Phase 2 RB-16).

set_back_policy (a_policy: INTEGER)

Decide who handles the Back key from now on.

Requires

valid: a_policy = Back_system or a_policy = Back_app

Ensures

set: back_policy = a_policy

keep_screen_on: BOOLEAN

Is the screen kept from dimming?

set_keep_screen_on (a_on: BOOLEAN)

Keep the screen awake while the app is shown (or stop).

Ensures

set: keep_screen_on = a_on

is_finishing: BOOLEAN

Has `finish' been asked for?

finish

Ask Android to end the app; `destroyed' follows.

Requires

not_destroyed: not lifecycle.is_destroyed

Ensures

finishing: is_finishing

Invariant

valid_back_policy: back_policy = Back_system or back_policy = Back_app services_consistent: screen.has_window = lifecycle.has_window

PHONE_SCREEN

The window's pixel buffer, one frame at a time. `present_argb' copies a cairo-format ARGB32 image (native-endian 0xAARRGGBB words) to the screen at (0,0), clipped. It is the one seam a GPU path would replace (research D-005). `has_window' is the live truth from Android; see SIMPLE_EIF_PHONE's invariant for why it matches the lifecycle model at every delivery.

Status

has_window: BOOLEAN

Does Android currently give us a window?

in_frame: BOOLEAN

Is the buffer locked for drawing?

width: INTEGER

Window width in pixels (0 without a window).

Ensures

non_negative: Result >= 0

height: INTEGER

Window height in pixels (0 without a window).

Ensures

non_negative: Result >= 0

Frame

begin_frame

Lock the buffer. Android may refuse: check `in_frame' after.

Requires

has_window: has_window not_nested: not in_frame

Ensures

sized_when_locked: in_frame implies (width > 0 and height > 0)

fill_rect (a_x, a_y, a_w, a_h, a_rgb: INTEGER)

Fill a rectangle with color `a_rgb' (0xRRGGBB), clipped to the window.

Requires

in_frame: in_frame size_ok: a_w >= 0 and a_h >= 0 rgb_ok: 0 <= a_rgb and a_rgb <= 0xFFFFFF

Ensures

still_in_frame: in_frame

present_argb (a_pixels: POINTER; a_width, a_height, a_stride: INTEGER)

Copy an ARGB32 image (`a_stride' bytes per row) to (0,0), clipped.

Requires

in_frame: in_frame pixels_exist: a_pixels /= default_pointer size_ok: a_width > 0 and a_height > 0 stride_ok: a_stride >= a_width * 4

Ensures

still_in_frame: in_frame

end_frame

Unlock and show the frame.

Requires

in_frame: in_frame

Ensures

not_in_frame: not in_frame

Testing

peek (a_x, a_y: INTEGER): NATURAL_32

Window buffer word at (`a_x', `a_y'); for byte-order tests only.

Requires

in_frame: in_frame inside: 0 <= a_x and a_x < width and 0 <= a_y and a_y < height

Invariant

frame_needs_window: in_frame implies has_window

PHONE_METRICS

Window size, density and the content rectangle: the area not covered by the status and navigation bars (or the on-screen keyboard). Insets are derived from it. Values are read from Android at `refresh'; SIMPLE_EIF_PHONE refreshes on window, configuration and content-rect events. Font scale is not here: the NDK has no getter for it (spec 03 A-6).

Access

width, height: INTEGER

Window size in pixels.

density_dpi: INTEGER

Screen density in dots per inch.

content_rect: PHONE_RECT

Area where content is seen by the user.

layout_is_rtl: BOOLEAN

Is the phone's layout direction right-to-left?

inset_left: INTEGER

Pixels covered on the left.

Ensures

non_negative: Result >= 0

inset_top: INTEGER

Pixels covered at the top (status bar).

Ensures

non_negative: Result >= 0

inset_right: INTEGER

Pixels covered on the right.

Ensures

non_negative: Result >= 0

inset_bottom: INTEGER

Pixels covered at the bottom (navigation bar, keyboard).

Ensures

non_negative: Result >= 0

dp (a_dp: INTEGER): INTEGER

`a_dp' density-independent pixels in real pixels (160 dpi baseline).

Requires

non_negative: a_dp >= 0

Ensures

non_negative: Result >= 0

Update

refresh

Re-read every value from Android. The content rectangle is clamped to the window; an empty one from Android (none reported yet) means the whole window (Phase 2 RB-4).

Ensures

clamped_across: content_rect.left >= 0 and content_rect.right <= width clamped_down: content_rect.top >= 0 and content_rect.bottom <= height empty_is_full: (width > 0 and height > 0) implies (content_rect.width > 0 and content_rect.height > 0) density_known: (width > 0 and height > 0) implies (120 <= density_dpi and density_dpi <= 640)

Invariant

sizes_non_negative: width >= 0 and height >= 0 and density_dpi >= 0 insets_fit_across: width > 0 implies inset_left + inset_right <= width insets_fit_down: height > 0 implies inset_top + inset_bottom <= height content_inside_across: width > 0 implies (content_rect.left >= 0 and content_rect.right <= width) content_inside_down: height > 0 implies (content_rect.top >= 0 and content_rect.bottom <= height)

PHONE_STORAGE

App-private folders on the phone. `internal_path' always exists and needs no permission; `external_path' may be absent.

Access

internal_path: STRING_8

The app's private files folder (UTF-8 path).

Ensures

absolute: not Result.is_empty implies Result.starts_with ("/")

external_path: detachable STRING_8

The app's folder on shared storage, if Android offers one.

Ensures

absolute: attached Result as al_r implies (not al_r.is_empty and al_r.starts_with ("/"))

PHONE_ASSETS

Read-only files packed in the APK's assets/ folder, by relative name (e.g. "fonts/noto.ttf"). Missing files are a normal outcome, not an error: `last_asset' is Void.

Status

has_asset (a_name: READABLE_STRING_8): BOOLEAN

Is `a_name' packed in the APK?

Requires

name_ok: is_valid_name (a_name)

is_valid_name (a_name: READABLE_STRING_8): BOOLEAN

Non-empty and relative.

Access

last_asset: detachable MANAGED_POINTER

Bytes from the last `read_asset', or Void if it was missing.

last_asset_size: INTEGER

Byte count of `last_asset' (0 if missing).

Basic operations

read_asset (a_name: READABLE_STRING_8)

Read `a_name' into `last_asset'.

Requires

name_ok: is_valid_name (a_name)

Ensures

found_has_data: attached last_asset as al_d implies al_d.count = last_asset_size missing_has_none: last_asset = Void implies last_asset_size = 0

Invariant

size_non_negative: last_asset_size >= 0

PHONE_LOG

Write lines to the Android log (logcat) under `tag'.

Access

tag: STRING_8

Log tag (what `adb logcat -s <tag>' filters on).

Settings

set_tag (a_tag: READABLE_STRING_8)

Use `a_tag' from now on.

Requires

not_empty: not a_tag.is_empty short: a_tag.count <= 23

Ensures

set: tag.same_string (a_tag)

Output

debug_line (a_text: READABLE_STRING_8)

Debug-level line.

info (a_text: READABLE_STRING_8)

Info-level line.

warn (a_text: READABLE_STRING_8)

Warning-level line.

error (a_text: READABLE_STRING_8)

Error-level line.

Invariant

tag_ok: not tag.is_empty and tag.count <= 23

PHONE_EVENT

One thing that happened on the phone: a lifecycle change, a touch or a key. Immutable. Exactly one family per event (or none, for a timed poll that ran out). Touch coordinates are window pixels, rounded; they may lie outside the window while a finger drags off the edge.

Access

kind: INTEGER

Event code (see PHONE_EVENT_KIND).

time_ms: INTEGER

Android uptime in milliseconds, masked to 31 bits by the glue: never negative; wraps to 0 after 2^31 ms (~24.8 days). Compare two times by their difference, not by `<'.

pointer_id: INTEGER

Finger id for touch events; -1 otherwise.

x, y: INTEGER

Window pixel position for touch events; 0 otherwise.

key_code: INTEGER

Android key code for key events; 0 otherwise.

Status

is_none: BOOLEAN

Is this "no event"?

is_lifecycle: BOOLEAN

Is this a lifecycle event?

is_touch: BOOLEAN

Is this a touch event?

is_key: BOOLEAN

Is this a key event?

Output

out_line: STRING_8

One-line description, e.g. "touch_down id=0 x=12 y=40 t=1234".

Ensures

starts_with_name: Result.starts_with (kind_name (kind)) one_line: not Result.has ('%N')

Invariant

valid_kind: is_valid_kind (kind) one_family: is_none.to_integer + is_lifecycle.to_integer + is_touch.to_integer + is_key.to_integer = 1 touch_has_id: is_touch implies pointer_id >= 0 non_touch_no_id: not is_touch implies pointer_id = -1 key_has_code: is_key = (key_code > 0) non_touch_no_position: not is_touch implies (x = 0 and y = 0) time_non_negative: time_ms >= 0

PHONE_EVENT_KIND

Event codes for SIMPLE_EIF_PHONE, grouped in three families: lifecycle (1-14), touch (20-23) and key (30-31). Code 0 means no event (a timed poll that ran out). The numbers are shared with the C glue (runtime/c/sephone.h); change both together.

Codes: none

Kind_none: INTEGER = 0

No event (timed poll ran out).

Codes: lifecycle

Kind_started: INTEGER = 1

Kind_resumed: INTEGER = 2

Kind_paused: INTEGER = 3

Kind_stopped: INTEGER = 4

Kind_destroyed: INTEGER = 5

Kind_window_ready: INTEGER = 6

Kind_window_lost: INTEGER = 7

Kind_window_resized: INTEGER = 8

Kind_redraw_needed: INTEGER = 9

Kind_focus_gained: INTEGER = 10

Kind_focus_lost: INTEGER = 11

Kind_configuration_changed: INTEGER = 12

Kind_low_memory: INTEGER = 13

Kind_content_rect_changed: INTEGER = 14

Codes: touch

Kind_touch_down: INTEGER = 20

Kind_touch_move: INTEGER = 21

Kind_touch_up: INTEGER = 22

Kind_touch_cancel: INTEGER = 23

Codes: key

Kind_key_down: INTEGER = 30

Kind_key_up: INTEGER = 31

Families

is_lifecycle_kind (a_k: INTEGER): BOOLEAN

Is `a_k' a lifecycle code?

is_touch_kind (a_k: INTEGER): BOOLEAN

Is `a_k' a touch code?

is_key_kind (a_k: INTEGER): BOOLEAN

Is `a_k' a key code?

is_valid_kind (a_k: INTEGER): BOOLEAN

Is `a_k' none or a member of exactly one family?

Ensures

definition: Result = (a_k = Kind_none or is_lifecycle_kind (a_k) or is_touch_kind (a_k) or is_key_kind (a_k)) families_disjoint: (is_lifecycle_kind (a_k).to_integer + is_touch_kind (a_k).to_integer + is_key_kind (a_k).to_integer) <= 1

Names

kind_name (a_k: INTEGER): STRING_8

Lower-case name of `a_k', for logs and tests (e.g. "touch_down").

Requires

valid: is_valid_kind (a_k)

Ensures

not_empty: not Result.is_empty

PHONE_KEY_CODES

Android key codes the layer names (values from android/keycodes.h). Inherit it to compare `last_event.key_code' by name.

Codes

Key_home: INTEGER = 3

Key_back: INTEGER = 4

Key_dpad_up: INTEGER = 19

Key_dpad_down: INTEGER = 20

Key_dpad_left: INTEGER = 21

Key_dpad_right: INTEGER = 22

Key_volume_up: INTEGER = 24

Key_volume_down: INTEGER = 25

Key_enter: INTEGER = 66

Key_del: INTEGER = 67

Key_menu: INTEGER = 82

PHONE_LIFECYCLE

Where the app is in Android's life, built from delivered events. Pure Eiffel: no platform calls, so it is tested on the PC. Lenient by design (Phase 2 RB-17): it accepts any order of events Android may send and only refuses use after `destroyed'. Each event changes exactly the state its kind names (per-kind frame clauses). `resumed' also sets `is_started' (Android always starts before it resumes), so the model stays consistent even if an event is lost.

Status

is_started: BOOLEAN

Between `started' and `stopped'?

is_resumed: BOOLEAN

Between `resumed' and `paused' (in the foreground)?

has_window: BOOLEAN

Between `window_ready' and `window_lost'?

has_focus: BOOLEAN

Between `focus_gained' and `focus_lost'?

is_destroyed: BOOLEAN

Has `destroyed' been applied? (final)

window_generation: INTEGER

Number of `window_ready' events so far; lets apps drop caches tied to an older window.

last_applied: detachable PHONE_EVENT

Most recent event passed to `apply' (any family).

affects_state (a_k: INTEGER): BOOLEAN

Does lifecycle code `a_k' change this model?

Element change

apply (a_e: PHONE_EVENT)

Update the model for `a_e'. Touch, key and the non-state lifecycle events (resized, redraw, configuration, low memory, content rect) change nothing but `last_applied'.

Requires

not_destroyed: not is_destroyed

Ensures

recorded: last_applied = a_e started: a_e.kind = Kind_started implies is_started started_frame: a_e.kind = Kind_started implies (is_resumed = old is_resumed and has_window = old has_window and has_focus = old has_focus) resumed: a_e.kind = Kind_resumed implies (is_started and is_resumed) resumed_frame: a_e.kind = Kind_resumed implies (has_window = old has_window and has_focus = old has_focus) paused: a_e.kind = Kind_paused implies not is_resumed paused_frame: a_e.kind = Kind_paused implies (is_started = old is_started and has_window = old has_window and has_focus = old has_focus) stopped: a_e.kind = Kind_stopped implies (not is_started and not is_resumed) stopped_frame: a_e.kind = Kind_stopped implies (has_window = old has_window and has_focus = old has_focus) window_in: a_e.kind = Kind_window_ready implies (has_window and window_generation = old window_generation + 1) window_in_frame: a_e.kind = Kind_window_ready implies (is_started = old is_started and is_resumed = old is_resumed and has_focus = old has_focus) window_out: a_e.kind = Kind_window_lost implies not has_window window_out_frame: a_e.kind = Kind_window_lost implies (is_started = old is_started and is_resumed = old is_resumed and has_focus = old has_focus) focus_in: a_e.kind = Kind_focus_gained implies has_focus focus_out: a_e.kind = Kind_focus_lost implies not has_focus focus_frame: (a_e.kind = Kind_focus_gained or a_e.kind = Kind_focus_lost) implies (is_started = old is_started and is_resumed = old is_resumed and has_window = old has_window) destroyed: a_e.kind = Kind_destroyed implies (is_destroyed and not is_started and not has_window and not has_focus) destroyed_only_by_destroy: a_e.kind /= Kind_destroyed implies not is_destroyed generation_only_on_window_ready: a_e.kind /= Kind_window_ready implies window_generation = old window_generation others_unchanged: not affects_state (a_e.kind) implies (is_started = old is_started and is_resumed = old is_resumed and has_window = old has_window and has_focus = old has_focus and is_destroyed = old is_destroyed)

Invariant

resumed_implies_started: is_resumed implies is_started destroyed_is_final: is_destroyed implies not (is_started or is_resumed or has_window or has_focus) generation_non_negative: window_generation >= 0

PHONE_TOUCHES

The fingers currently on the glass, by pointer id, with their last positions. Built from delivered touch events. Pure Eiffel, PC-tested. A move for an unknown id (its down was lost) is ignored; any `touch_cancel' clears every finger.

Model

active_ids: MML_SET [INTEGER]

Ids of the fingers currently down.

xs_model: MML_MAP [INTEGER, INTEGER]

Last x of each finger down, by id (Phase 2 RB-12).

ys_model: MML_MAP [INTEGER, INTEGER]

Last y of each finger down, by id (Phase 2 RB-12).

Access

count: INTEGER

Number of fingers down.

is_active (a_id: INTEGER): BOOLEAN

Is finger `a_id' down?

Ensures

definition: Result = active_ids [a_id]

x_of (a_id: INTEGER): INTEGER

Last x of finger `a_id'.

Requires

active: is_active (a_id)

Ensures

definition: Result = xs_model [a_id]

y_of (a_id: INTEGER): INTEGER

Last y of finger `a_id'.

Requires

active: is_active (a_id)

Ensures

definition: Result = ys_model [a_id]

last_applied: detachable PHONE_EVENT

Most recent event passed to `apply' (any family).

Element change

apply (a_e: PHONE_EVENT)

Update the fingers for `a_e'. Losing the window or focus, or being destroyed, lifts every finger (Phase 2 RB-11: Android is not known to send a cancel then). Other non-touch events change nothing but `last_applied'.

Ensures

recorded: last_applied = a_e down: a_e.kind = Kind_touch_down implies (active_ids |=| (old active_ids & a_e.pointer_id) and x_of (a_e.pointer_id) = a_e.x and y_of (a_e.pointer_id) = a_e.y) down_positions: a_e.kind = Kind_touch_down implies (xs_model |=| (old xs_model).updated (a_e.pointer_id, a_e.x) and ys_model |=| (old ys_model).updated (a_e.pointer_id, a_e.y)) move: (a_e.kind = Kind_touch_move and old is_active (a_e.pointer_id)) implies (active_ids |=| old active_ids and x_of (a_e.pointer_id) = a_e.x and y_of (a_e.pointer_id) = a_e.y) move_positions: (a_e.kind = Kind_touch_move and old is_active (a_e.pointer_id)) implies (xs_model |=| (old xs_model).updated (a_e.pointer_id, a_e.x) and ys_model |=| (old ys_model).updated (a_e.pointer_id, a_e.y)) stray_move_ignored: (a_e.kind = Kind_touch_move and not old is_active (a_e.pointer_id)) implies (active_ids |=| old active_ids and xs_model |=| old xs_model and ys_model |=| old ys_model) up: a_e.kind = Kind_touch_up implies active_ids |=| (old active_ids / a_e.pointer_id) up_positions: a_e.kind = Kind_touch_up implies (xs_model |=| (old xs_model).removed (a_e.pointer_id) and ys_model |=| (old ys_model).removed (a_e.pointer_id)) cancel: a_e.kind = Kind_touch_cancel implies active_ids.is_empty cleared: (a_e.kind = Kind_window_lost or a_e.kind = Kind_focus_lost or a_e.kind = Kind_destroyed) implies active_ids.is_empty non_touch_unchanged: (not a_e.is_touch and not clears_touches (a_e.kind)) implies (active_ids |=| old active_ids and xs_model |=| old xs_model and ys_model |=| old ys_model)

clears_touches (a_k: INTEGER): BOOLEAN

Does a non-touch event of kind `a_k' lift every finger?

Invariant

count_matches_model: count = active_ids.count positions_cover_ids: xs_model.domain |=| active_ids and ys_model.domain |=| active_ids

PHONE_RECT

A pixel rectangle: left/top inclusive, right/bottom exclusive. Immutable.

Access

left, top, right, bottom: INTEGER

width: INTEGER

`right' - `left'.

Ensures

definition: Result = right - left

height: INTEGER

`bottom' - `top'.

Ensures

definition: Result = bottom - top

Invariant

ordered: left <= right and top <= bottom