package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c.kernel/Frama_c_kernel/Linear/Space/Vector/index.html

Module `Space.Vector`

val pretty : Stdlib.Format.formatter -> 'n vector -> unit

val zero : 'n Nat.succ Nat.nat -> 'n Nat.succ vector

The call zero n returns the 0 vector in 𝕂ⁿ.

val repeat : scalar -> 'n Nat.succ Nat.nat -> 'n Nat.succ vector

The call repeat x n returns a vector in 𝕂ⁿ which each dimension containing the scalar x.

val base : 
  'n Nat.succ Finite.finite ->
  'n Nat.succ Nat.nat ->
  'n Nat.succ vector

The call base i n returns the i-th base vector in the orthonormal space of 𝕂ⁿ. In other words, the returned vector contains zero except for the i-th coordinate, which contains one.

val get : 'n Finite.finite -> 'n vector -> scalar

The call get i m returns the i-th coefficient.

val set : 'n Finite.finite -> scalar -> 'n vector -> 'n vector

The call set i x v returns a new vector of the same linear space as v, and with the same coordinates, except for the i-th one, which is set to the scalar x.

val size : 'n vector -> 'n Nat.nat

The call size v for v a vector of 𝕂ⁿ returns n.

val norm : 'n vector -> scalar

The call norm v computes the ∞-norm of v, i.e the maximum of the absolute values of its coordinates.

val max : 'n vector -> 'n vector -> 'n vector

The call max l r returns a vector for which each coordinate is the maximum between the corresponding coordinates of l and r.