Image Calculator

Overview

Image processing attempts to enhance certain features in images and suppress others. An image calculator evaluates formulas that operate on image sequences. Basic operations in these formulas expect sequences of images as operands and deliver sequences of images as values. Operands of some basic operations include image transformers, in addition to image sequences. This document describes the formulas and image representations supported by the image calculator to be delivered as a software product.

Displayable Images

Images are supplied as files in BMP format. All images are monochrome, one byte per pixel. Each pixel-byte represents an integer between 0 and 255. The pixel-byte is interpreted as the unsigned binary numeral for the linear, grayscale number it represents. Image resolution in the x-y plane is specified as part of the image representation. The steganography project discusses the BMP file format and reading them as byte sequences.

Image sequences for testing are available in the BMPimages directory. Bottom-level folders in the directory contain sequences of BMP files, and each of the BMP files represents an image. File names are chosen to indicate ordering of the images within the sequence. All of the supplied images depict biological specimens, and all but one were acquired using Olympus Fluoview, laser scanning, confocal, fluorescent-light microscopes. The other was acquired using a more primitive microscope without confocal imaging.

Representation of images for software operations is up to you. The chosen representation will need to specify a two dimensional array of pixels, each of which specifies a grayscale number in the range 0 to 255.

Computed Images

For computational purposes, images are converted to pixel-arrays in which each pixel is a rational number. These rational numbers have no fixed relationship to displayable grayscale values. The person using the calculator will decide how to scale computed images to 8-bit, grayscale values for display purposes.

Basic Operations

Convert Displayable Image to Computed Image
Operand	displayable-image sequence
Result	computed-image sequence Each pixel in the result is the rational number represented by the corresponding pixel in the image. Any color palette that may have been specified for the displayable image is lost in the result

Convert Computed Image to Displayable Image
Operands	1. offset – a rational number 2. divisor – a rational number 3. computed-image sequence
Result	displayable-image sequence Each pixel in the result is computed by adding the offset supplied in the first operand to the number represented by the corresponding pixel in the image supplied as the third operand, then dividing that sum by the divisor supplied as the second operand, rounding to the nearest integer, and clipping to the range 0 to 255 If color-palette is part of the displayable image representation, it should specify a linear grayscale

Image Scaling
Operands	1. offset – a rational number 2. divisor – a rational number 3. computed-image sequence
Result	computed-image sequence Each pixel in the result is computed by adding the offset supplied in the first operand to the number represented by the corresponding pixel in the image supplied as the third operand, then dividing that sum by the divisor supplied as the second operand

Image Addition
Operands	1. computed-image sequence 2. computed-image sequence
Result	computed-image sequence A pixel in the result is computed by adding the numbers represented by corresponding pixels in the image sequences supplied as operands If the first operand contains a different number of images than the second operand, the shorter image sequence is interpreted as if it were repeated enough times to make the two image sequences the same length If two corresponding images have different resolutions, they are interpreted as if the pixels at index (0,0) were aligned and non-overlapping pixels were discarded The x-resolution (y-resolution) of the resulting image is the smaller of the x-resolutions (y-resolutions) of the operand images

Image Subtraction
Operands	1. computed-image sequence 2. computed-image sequence
Result	computed-image sequence A pixel in the result is computed by subtracting the number represented by a pixel in the image supplied as the second operand from the number represented by the corresponding pixel in the image supplied as the first operand Differences in length between the image sequences and between the resolutions of corresponding images are handled as in image addition

Image Ratio
Operands	1. computed-image sequence 2. computed-image sequence
Result	computed-image sequence A pixel in the result is computed by dividing the number represented by a pixel in the image supplied as the first operand by the number represented by the corresponding pixel in the image supplied as the second operand If a pixel representing the number 0 occurs in the second image sequence, treat it as if it were a 1 Differences in length between the image sequences and between the resolutions of corresponding images are handled as in image addition

Image Filtering
Operand	filter - a square matrix of rational numbers together with a divisor
Result	computed-image sequence A pixel in the result is computed by centering the filter over the corresponding pixel in the image supplied as the second operand, multiplying the numbers represented by pixels in the image by the filter values that align with those pixels, summing the resulting products, and dividing by the product of the divisor supplied in the filter Near the border of the image, the centered filter will have elements for which the corresponding pixel in the image is missing The operation interprets missing pixel values as zeros

Image and Filter Input

The get-image function, which may be invoked only to specify a top-level argument in an image formula, constructs a displayable-image sequence from a sequence of BMP files. The argument of the get-image function is a string specifying a directory containing a sequence of BMP image files. The function delivers the displayable-image sequence represented by the files in the directory. The representation of the displayable-image sequence delivered by the get-image function is up to the software designer.

The get-filter function, which may be invoked only to specify top-level in arguments in image commands, constructs a filter from a file. Filter files are Unix-style text files with an ICK extension (INDEC Convolution Kernel). Filter files for testing are available in the Filters directory.

The argument of the get-filter function is a string specifying a path to a filter file. The function delivers a square, two-dimensional matrix of numbers representing the filter specified in the file. The representation of this two-dimensional matrix is up to you.

If the file specifies a filter with no center (that is, a filter with an even number of rows), add a row and column of zeros to make it have a center element. If the file fails to specify enough numbers for the filter, assume the missing numbers are zeros, and put them in the trailing rows (and at the trailing end of the first row for which numbers are not supplied). If the file specifies too many numbers for the filter, ignore the trailing numbers.

Image Output

The put-image function has three arguments: (1) a string specifying a directory in the file system, (2) a string specifying a prefix to be used for the names of the displayable image-files to be written, and (3) a sequence of displayable images. The put-image function, which may be invoked only at the top level in image commands, writes a sequence of BMP image files in the directory specified by the string supplied as its first argument. For each image in the sequence supplied by the third argument, the put-image function writes a BMP file representing that image. Names given to the files are decimal numerals prefixed by the string supplied as the second argument. A numeral representing zero is used for the first image in the sequence, and successive numerals are used for successive images in the sequence.

Image Formulas

Image formulas are ACL2 expression in which the function is a lambda expression and the arguments are displayable-image sequences, filters, or numbers that are appropriate for the lambda expression.

Arguments in image formulas that represent displayable-image sequences may be constructed by invocations of theget-image function. Filter arguments may be constructed by invocations of the get-filter function. Numbers are specified as ACL2 rationals. Functions in lambda expressions must be basic image operators.

Example image formula

((lambda (filter image1 image2)
    (comp->disp 5
                250/100
                (image-filter filter
                              (image-add (disp->comp image1)
                                         (disp->comp image2)))))
   (get-filter "c:/filters/5X5Corner.ick")
   (get-image "c:/BMPimages/Kidney/Green/")
   (get-image "c:/BMPimages/Kidney/Red/"))

Image Commands

An image command is an ACL2 expressions in which the function is put-image and the arguments are a destination directory, an image-name prefix, and an image formula.

Example image command

(put-image "c:/BMPimages/Kidney/Filtered"
           "kidney-combo"
           ((lambda (filter image1 image2)
               (comp->disp  256
                            25/10
                            (image-filter filter 
                                          (image-add (disp->comp image1)
                                                     (disp->comp image2)))))
             (get-filter "c:/filters/5X5Corner.ick")
             (get-image "c:/BMPimages/Kidney/Green/")
             (get-image "c:/BMPimages/Kidney/Red/")))

Tests and Theorems

As a minimum, every function be accompanied by tests and theorems that state that if the function is supplied with arguments with the expected kind, it will deliver values of the expected kind.

Optional Extensions

The image calculator supports anonymous functions through lambda expressions. It would be nice if it supported definitions (and invocations) of named functions.